diff --git a/src/mapping.v b/src/mapping.v
index be78184..2fc4d83 100644
--- a/src/mapping.v
+++ b/src/mapping.v
@@ -46,6 +46,47 @@ Qed.
  *)
 
 
+Lemma permutation_mapping_nil {X: Type} :
+  forall (base : list X), permutation_mapping nil nil base.
+Proof.
+  intro base. exists base. exists nil. split; easy.
+Qed.
+
+
+Lemma permutation_mapping_nil_l {X: Type} :
+  forall (u base : list X), permutation_mapping nil u base -> u = nil.
+Proof.
+  intro u. induction u; intro base; intro H. reflexivity.
+  destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
+  inversion H1. symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H3.
+  inversion H3.
+Qed.
+
+
+Lemma permutation_mapping_nil_r {X: Type} :
+  forall (u base : list X), permutation_mapping u nil base -> u = nil.
+Proof.
+  intro u. induction u; intro base; intro H. reflexivity.
+  destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
+  inversion H1. symmetry in H3. apply map_eq_nil in H3. rewrite H3 in H0.
+  inversion H0.
+Qed.
+
+
+Lemma permutation_mapping_cons {X: Type} :
+  forall (u v base : list X) a b,
+    permutation_mapping (a::u) (b::v) base -> permutation_mapping u v base.
+Proof.
+  intros u v base a b. intro H. destruct H as [p]. destruct H as [l].
+  destruct H. destruct H0. exists p. destruct l. inversion H0. exists l.
+  split. assumption. split; [ inversion H0 | inversion H1]; reflexivity.
+Qed.
+
+
+
+
+
+
 Lemma permutation_mapping_self {X: Type} :
   forall (u base : list X), incl u base -> permutation_mapping u u base.
 Proof.
@@ -177,9 +218,7 @@ Proof.
   intros m n f' g'. intros J J1 J2 J3.
 
   rewrite H6. apply J2 in J3. destruct J3. apply H9. apply J. assumption.
-
   rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6.
-
   symmetry. rewrite map_nth_error with (d := f a). reflexivity.
 
   rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity.
@@ -206,10 +245,6 @@ Qed.
 
 
 
-
-
-
-(*
 Lemma permutation_mapping_base {X: Type} :
   forall (u v base p: list X),
     Permutation base p -> permutation_mapping u v base
@@ -233,8 +268,6 @@ Proof.
   apply FinFun.bSurjective_bBijective in H4. destruct H4 as [g].
   destruct H4.
 
-
-
   exists base. exists (map g l). split.
   apply Permutation_trans with (l' := base). apply Permutation_sym.
   assumption. apply Permutation_refl. split.
@@ -269,9 +302,9 @@ Proof.
   intro s. induction s; intros t; intros M1 M2.
   apply in_nil in M2. contradiction.
   apply in_inv in M2. destruct M2. rewrite H9 in M1.
-  destruct t. inversion M1. inversion M1. easy.
-  destruct t. inversion M1. inversion M1.
-  apply IHs with (t := t). assumption. assumption.
+  destruct t; inversion M1. easy.
+  destruct t; inversion M1.
+  apply IHs with (t := t); assumption.
   generalize N. generalize H1. apply H9.
 
   (* second case in split *)
@@ -284,7 +317,29 @@ Proof.
 
   rewrite nth_error_nth' with (d := x).
   rewrite nth_error_nth' with (d := x).
-  replace a with (g (f a)) at 1.
+
+  rewrite Permutation_nth in H0. destruct H0. destruct H7 as [h].
+  destruct H7. destruct H8.
+  apply FinFun.bInjective_bSurjective in H8.
+  apply FinFun.bSurjective_bBijective in H8. destruct H8 as [h'].
+  destruct H8.
+
+  rewrite H9.
+
+  assert (forall n, n < length base -> h n = g n).
+  intro n. intro J.
+
+
+
+
+
+
+
+
+
+
+
+  replace a with (f (g a)) at 1.
   rewrite <- H5. reflexivity.
   apply H4. assumption.
   apply H6 in M. destruct M. assumption.