Update

src/mapping.v

@@ -319,38 +319,6 @@ Proof.
   rewrite <- H6. rewrite IHb. reflexivity.
   rewrite seq_shift. rewrite cons_seq. reflexivity. apply H6.
 
-
-
-
-
-
-
-
-
-
-
-
-
-  exists (map (fun e => (nth (g e) base x)) (seq 0 (length base))).
-  exists (map f l). split.
-
-
-
-
-  apply Permutation_sym. apply nat_bijection_Permutation.
-
-
-  rewrite Permutation_image.
-
-  assert (forall (b: list X),
-    Permutation b (map (fun e => nth (g e) b x) (seq 0 (length b)))).
-  intro b. induction b. easy.
-  replace (seq 0 (length (a::b))) with ((seq 0 (length b)) ++ [ length b ]).
-  rewrite map_app.
-
-
-
-  admit. (* TODO *) (* easy. *)
   split.
 
   (* first case in split *)