diff --git a/src/mapping.v b/src/mapping.v
index 10faaf2..a2effea 100644
--- a/src/mapping.v
+++ b/src/mapping.v
@@ -19,11 +19,11 @@ Definition permutation_mapping {X: Type} (u v base : list X) :=
 
 
 
+(*
 
 Definition incl_without_eq {X: Type} (u v : list X) :=
   exists l, map Some u = map (nth_error v) l.
 
-
 Lemma incl_without_eq_incl {X: Type}:
   forall (u v : list X), incl_without_eq u v -> incl u v.
 Proof.
@@ -43,7 +43,7 @@ Proof.
   apply In_nth_error in H. destruct H. exists (x0 :: x).
   simpl. rewrite H. rewrite H0. reflexivity.
 Qed.
-
+ *)
 
 
 Lemma permutation_mapping_self {X: Type} :
@@ -57,3 +57,29 @@ Proof.
 Qed.
 
 
+Lemma permutation_mapping_length {X: Type} :
+  forall (u v base : list X),
+  permutation_mapping u v base -> length u = length v.
+Proof.
+  intros u v base. intro H. destruct H. destruct H. destruct H. destruct H0.
+  replace (length u) with (length (map Some u)). rewrite H0.
+  replace (length v) with (length (map Some v)). rewrite H1.
+  rewrite map_length. rewrite map_length. reflexivity.
+  apply map_length. apply map_length.
+Qed. 
+
+
+Lemma permutation_mapping_swap {X: Type} :
+  forall (u v base : list X),
+  permutation_mapping u v base -> permutation_mapping v u base.
+Proof.
+  intro u. induction u; intros v base; intro H.
+
+
+
+
+
+
+
+
+