Update

src/mapping.v

@@ -348,20 +348,12 @@ Proof.
   (* second case in split *)
   rewrite H0.
 
-  (*
-  apply FinFun.bInjective_bSurjective in H3.
-  apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
-  destruct H3.
-   *)
-
   assert (forall s, (forall y, In y s -> y < length base)
     -> map (nth_error base) s
       = map (nth_error (map (fun e => nth (g e) base x) (seq 0 (length base)))) (map f s)).
   intro s. rewrite map_map. induction s; intro K. reflexivity.
   simpl. rewrite IHs.
 
-
-
   assert (forall q p, p < q -> nth p (seq 0 q) 0 = p).
   intro q. induction q; intro p'; intro J4.
   apply Nat.nlt_0_r in J4. contradiction.
@@ -378,7 +370,6 @@ Proof.
     with (Some ((fun e => nth (g e) base x)
                 (nth (f a) (seq 0 (length base)) 0))).
 
-
   assert (forall m n f' g',
     FinFun.bFun m f' -> FinFun.bFun m g'
     -> (forall x : nat, x < m -> g' (f' x) = x /\ f' (g' x) = x)
@@ -389,9 +380,10 @@ Proof.
 
   rewrite H6. apply H5 in N. destruct N. rewrite H8. reflexivity.
   apply H2. assumption. rewrite H6. apply H5 in N. destruct N.
-  rewrite H7.
 
-  rewrite nth_error_nth' with (d := x).
+  symmetry. rewrite map_nth_error with (d := f a). reflexivity.
+
+  rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity.