diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 059dd8b70faddc510e9c24fad59ad3160e895c8c..c02ae96b06709a1340090c908b3d05af0bbad0ff 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -722,41 +722,62 @@ fold n in Hlb; fold n; destruct n as [|n].
 exists (fun_from_I_0 'I_0); [apply fun_from_I_0_inj |].
 rewrite (size0nil Hlb) (size0nil size_ord_enum); easy.
 (* n>0 *)
-pose (In1 := ord_enum n.+1); fold In1.
+pose (In := ord_enum n.+1); fold In.
 move: (perm_sortP HT2 HT1 HT0 _ _ Hla) => Hlc.
-pose (s := sort leT l2); assert (Hs1 : sort leT l1 = s) by easy.
-assert (Hs2 : size s = n.+1) by now rewrite size_sort.
-(* il1 and p1. *)
+pose (s := sort leT l2); assert (Hsa : sort leT l1 = s) by easy.
+assert (Hsb : size s = n.+1) by now rewrite size_sort.
+(* il1 and p1/q1. *)
 destruct (perm_ord_enum_sort leT x0 l1) as [il1 [Hil1a Hil1b] Hil1c].
-rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In1 in Hil1a; rewrite Hs1 in Hil1c.
+rewrite Hlb in il1, Hil1a, Hil1b, Hil1c; fold In in Hil1a; rewrite Hsa in Hil1c.
 assert (Hil1d : size il1 = n.+1) by now rewrite (perm_size Hil1a) size_ord_enum.
 pose (p1 := fun i : 'I_n.+1 => nth ord0 il1 i).
+assert (Hil1e : il1 = map p1 In).
+  unfold p1, In; move: (map_nth_ord_enum ord0 il1) => H.
+  rewrite -{1}H Hil1d; easy.
+rewrite Hil1e in Hil1c.
 assert (Hp1 : injective p1)
   by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil1d.
 pose (q1 := f_inv (injF_bij Hp1) : 'I_[n.+1]).
-assert (Hs3 : l1 = map ((nth x0 s) \o q1) In1).
-  rewrite -(map_nth_ord_enum x0 (map _ _)).
-  
-
-
-(*
+assert (Hs1 : l1 = map ((nth x0 s) \o q1) In).
+  apply (@eq_from_nth _ x0).
+  rewrite size_map size_ord_enum; easy.
+  intros i Hi; rewrite Hlb in Hi; pose (ii := Ordinal Hi).
+  assert (Hii : val ii < size In) by now rewrite size_ord_enum.
+  assert (Hq1ii : q1 ii < size In) by now rewrite size_ord_enum.
+  replace i with (val ii) by easy.
+  rewrite (nth_map ord0)//.
+  rewrite nth_ord_enum comp_correct Hil1c (nth_map ord0);
+      [f_equal | rewrite size_map; easy].
+  rewrite (nth_map ord0)// nth_ord_enum f_inv_correct_r; easy.
+(* il2 and p2/q2. *)
 destruct (perm_ord_enum_sort leT x0 l2) as [il2 [Hil2a Hil2b] Hil2c].
-rewrite Hn in il2, Hil2a, Hil2b, Hil2c.
+rewrite Hn in il2, Hil2a, Hil2b, Hil2c; fold In in Hil2a; fold s in Hil2c.
 assert (Hil2d : size il2 = n.+1) by now rewrite (perm_size Hil2a) size_ord_enum.
 pose (p2 := fun i : 'I_n.+1 => nth ord0 il2 i).
+assert (Hil2e : il2 = map p2 In).
+  unfold p2, In; move: (map_nth_ord_enum ord0 il2) => H.
+  rewrite -{1}H Hil2d; easy.
+rewrite Hil2e in Hil2c.
 assert (Hp2 : injective p2)
   by now move=>> /eqP H; apply /eqP; move: H; rewrite (nth_uniq ord0)// Hil2d.
 pose (q2 := f_inv (injF_bij Hp2) : 'I_[n.+1]).
+assert (Hs2 : l2 = map ((nth x0 s) \o q2) In).
+  apply (@eq_from_nth _ x0).
+  rewrite size_map size_ord_enum; easy.
+  intros i Hi; rewrite Hn in Hi; pose (ii := Ordinal Hi).
+  assert (Hii : val ii < size In) by now rewrite size_ord_enum.
+  assert (Hq2ii : q2 ii < size In) by now rewrite size_ord_enum.
+  replace i with (val ii) by easy.
+  rewrite (nth_map ord0)//.
+  rewrite nth_ord_enum comp_correct Hil2c (nth_map ord0);
+      [f_equal | rewrite size_map; easy].
+  rewrite (nth_map ord0)// nth_ord_enum f_inv_correct_r; easy.
 (* *)
 exists (q2 \o p1); [apply inj_comp; [apply f_inv_inj | easy] |].
 rewrite map_comp.
 
 
-replace (map (fun i : 'I_n.+1 => nth x0 l2 i) (map (q2 \o p1) (ord_enum n.+1)))
-    with (map (fun i : 'I_n.+1 => nth x0 l2 i) (map q2 (map p1 (ord_enum n.+1)))).
-rewrite (map_comp q2 p1).
-
-(_ -> _ = _) in seq
+(*
 
 HERE!
 *)