diff --git a/FEM/Algebra/Finite_table.v b/FEM/Algebra/Finite_table.v
index baad929733bc16fab2059520ddeacb816b31f1b9..795b675527e7b6d764f9ab6ee4a176e41162edf5 100644
--- a/FEM/Algebra/Finite_table.v
+++ b/FEM/Algebra/Finite_table.v
@@ -235,7 +235,7 @@ Definition neqxT {m n} (M N : 'E^{m,n}) i0 j0 : Prop :=
 Definition castTr {m1 m2 n} Hm (M : 'E^{m1,n}) : 'E^{m2,n} := castF Hm M.
 
 Definition castTc {m n1 n2} Hn (M : 'E^{m,n1}) : 'E^{m,n2} :=
-  fun i => castF Hn (M i).
+  mapF (castF Hn) M.
 
 Definition castT {m1 m2 n1 n2} Hm Hn (M : 'E^{m1,n1}) : 'E^{m2,n2} :=
   castTr Hm (castTc Hn M).
@@ -951,6 +951,56 @@ Lemma castT_id :
   forall {m n} {Hm : m = m} {Hn : n = n}, castT Hm Hn = @id 'E^{m,n}.
 Proof. intros; unfold castT; rewrite castTc_id castTr_id; easy. Qed.
 
+Lemma castTr_comp :
+  forall {m1 m2 m3 n} (Hm12 : m1 = m2) (Hm23 : m2 = m3) (M1 : 'E^{m1,n}),
+    castTr Hm23 (castTr Hm12 M1) = castTr (eq_trans Hm12 Hm23) M1.
+Proof. intros; apply castF_comp. Qed.
+
+Lemma castTc_comp :
+  forall {m n1 n2 n3} (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m,n1}),
+    castTc Hn23 (castTc Hn12 M1) = castTc (eq_trans Hn12 Hn23) M1.
+Proof. intros; apply extF; intro; apply castF_comp. Qed.
+
+Lemma castT_comp :
+  forall {m1 m2 m3 n1 n2 n3} (Hm12 : m1 = m2) (Hm23 : m2 = m3)
+      (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
+    castT Hm23 Hn23 (castT Hm12 Hn12 M1) =
+      castT (eq_trans Hm12 Hm23) (eq_trans Hn12 Hn23) M1.
+Proof.
+intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
+rewrite castTr_comp castTc_comp; easy.
+Qed.
+
+Lemma castT_comp_rl :
+  forall {m1 m2 m3 n1 n2}
+      (Hm12 : m1 = m2) (Hm23 : m2 = m3) (Hn : n1 = n2) (M1 : 'E^{m1,n1}),
+    castTr Hm23 (castT Hm12 Hn M1) = castT (eq_trans Hm12 Hm23) Hn M1.
+Proof. intros; unfold castT; rewrite castTr_comp; easy. Qed.
+
+Lemma castT_comp_rr :
+  forall {m1 m2 m3 n1 n2}
+      (Hm12 : m1 = m2) (Hm23 : m2 = m3) (Hn : n1 = n2) (M1 : 'E^{m1,n1}),
+    castT Hm23 Hn (castTr Hm12 M1) = castT (eq_trans Hm12 Hm23) Hn M1.
+Proof.
+intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
+rewrite castTr_comp; easy.
+Qed.
+
+Lemma castT_comp_cl :
+  forall {m1 m2 n1 n2 n3}
+      (Hm : m1 = m2) (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
+    castTc Hn23 (castT Hm Hn12 M1) = castT Hm (eq_trans Hn12 Hn23) M1.
+Proof.
+intros; unfold castT; rewrite -castT_equiv_def; unfold castT.
+rewrite castTc_comp; easy.
+Qed.
+
+Lemma castT_comp_cr :
+  forall {m1 m2 n1 n2 n3}
+      (Hm : m1 = m2) (Hn12 : n1 = n2) (Hn23 : n2 = n3) (M1 : 'E^{m1,n1}),
+    castT Hm Hn23 (castTc Hn12 M1) = castT Hm (eq_trans Hn12 Hn23) M1.
+Proof. intros; unfold castT; rewrite castTc_comp; easy. Qed.
+
 Lemma castTr_can :
   forall {m1 m2 n} (Hm12 : m1 = m2) (Hm21 : m2 = m1),
     cancel (@castTr E _ _ n Hm12) (castTr Hm21).
@@ -1761,7 +1811,7 @@ Lemma concatT_castT :
         (concatT M11 M12 M21 M22).
 Proof.
 intros; subst; apply extT; move=>>; rewrite 4!castT_refl.
-unfold castT, castTr, castTc, castF; f_equal; apply ord_inj; easy.
+unfold castT, castTr, castTc, castF, mapF, mapiF; f_equal; apply ord_inj; easy.
 Qed.
 
 Lemma concatTr_castTc :
diff --git a/FEM/FE.v b/FEM/FE.v
index 1b5c80ea3fed9db515205a2b2cacdffed854da4e..d0e5ce18e5d3758324f1cb81ef99c54ad329e5c9 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -50,6 +50,11 @@ Definition nvtx_of_shape (d : nat) (shape : shape_type) : nat :=
     | Quad => 2^d
   end.
 
+Lemma nos_eq :
+  forall {d1 d2 s1 s2},
+    d1 = d2 -> s1 = s2 -> nvtx_of_shape d1 s1 = nvtx_of_shape d2 s2.
+Proof. move=>>; apply f_equal2. Qed.
+
 (* TODO: add an admissibility property for the geometrical element?
   Il manque peut-être des hypothèses géométriques 
     du type triangle pas plat ou dim (span_as vertex) = d. 
@@ -76,13 +81,13 @@ Record FE : Type := mk_FE {
 Lemma FE_ext :
   forall {fe1 fe2 : FE} (Hd : d fe2 = d fe1)
       (Hn : ndof fe2 = ndof fe1) (Hs : shape fe2 = shape fe1),
-    vtx fe1 = castF (f_equal2 nvtx_of_shape Hd Hs) (mapF (castF Hd) (vtx fe2)) ->
+    vtx fe1 = castT (nos_eq Hd Hs) Hd (vtx fe2) ->
     P_approx fe1 = cast2F_fun Hd (P_approx fe2) ->
     Sigma fe1 = castF Hn (mapF (cast2F_fun Hd) (Sigma fe2)) ->
     fe1 = fe2.
 Proof.
 intros fe1 fe2 Hd Hn Hs; destruct fe1, fe2; simpl in *; subst.
-rewrite !castF_id !cast2F_fun_id; intros; subst.
+rewrite castT_id !cast2F_fun_id castF_id; intros; subst.
 f_equal; apply proof_irrel.
 Qed.
 
diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index d7f73f61514991728bd06b32754618d2e0fe167a..1d6ca36af48b7109e6d570464ca536ff5910e88a 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -647,39 +647,29 @@ Lemma FE_cur_eq : forall (vtx_cur :'R^{dL.+1,dL})
     FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx.
 Proof.
 intros vtx_cur Hvtx.
-pose (fe1:=FE_LagPk_d_cur dL kL dL_pos kL_pos vtx_cur Hvtx).
-pose (fe2:= FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx).
-fold fe1; fold fe2.
+pose (fe1 := FE_LagPk_d_cur dL kL dL_pos kL_pos vtx_cur Hvtx); fold fe1.
+pose (fe2 := FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx); fold fe2.
 assert (Hd : d fe2 = d fe1) by easy.
-assert (Hndof : ndof fe2 = ndof fe1) by easy.
+assert (Hn : ndof fe2 = ndof fe1) by easy.
 assert (Hs : shape fe2 = shape fe1) by easy.
-apply FE_ext with Hd Hndof Hs.
-apply extF; intros i; apply extF; intros j.
-unfold castF; simpl; rewrite mapF_correct; f_equal; apply ord_inj; easy.
+apply (FE_ext Hd Hn Hs); simpl.
 (* *)
-unfold cast2F_fun, castF_fun; simpl; apply subset_ext_equiv; split; intros p Hp.
+rewrite castT_comp_rr castT_id; easy.
+(* *)
+rewrite cast2F_fun_id; apply subset_ext_equiv; split; intros p Hp.
 (* . *)
-apply P_approx_k_d_compose_affine_mapping; try easy.
-eapply  is_affine_mapping_ext.
-2: apply (T_geom_is_affine_mapping vtx_cur).
-intros x; apply extF; intros i; unfold castF.
-f_equal; apply ord_inj; easy.
+simpl; apply P_approx_k_d_compose_affine_mapping; try easy.
+apply T_geom_is_affine_mapping.
 (* . *)
+simpl in Hp.
 apply P_approx_k_d_affine_mapping_rev with (T_geom vtx_cur); try easy.
 apply T_geom_is_affine_mapping.
 apply T_geom_bijective; easy.
-eapply P_approx_k_d_ext with (2:=Hp).
-unfold cur_to_ref; intros x; unfold compose; f_equal.
-apply extF; intros i; unfold castF; f_equal; apply ord_inj; easy.
 (* *)
-unfold cast2F_fun, castF_fun; apply extF; intros i.
+rewrite castF_id cast2F_fun_id; apply extF; intros i.
 rewrite mapF_correct; apply fun_ext; intros p; simpl.
-unfold Sigma_LagPk_d_cur, Sigma_nodal.
-unfold cur_to_ref, castF; f_equal.
-apply extF; intros j.
-rewrite -T_geom_transports_nodes; try easy; f_equal.
-2: apply ord_inj; easy.
-unfold node_ref_aux; f_equal; apply ord_inj; easy.
+unfold Sigma_LagPk_d_cur, Sigma_nodal, cur_to_ref; f_equal.
+rewrite T_geom_transports_nodes; easy.
 Qed.
 
 Lemma shape_fun_L_cur_eq : forall (vtx_cur :'R^{dL.+1,dL})
diff --git a/FEM/FE_simplex.v b/FEM/FE_simplex.v
index 7be549844a7d5dc575d40e1e64858cd8626f2b77..4d74bd3fa3a1d7e11a9ed7fc1ac747b16f4d5ca6 100644
--- a/FEM/FE_simplex.v
+++ b/FEM/FE_simplex.v
@@ -91,11 +91,7 @@ Proof.
 apply (nvtx_Simplex FE_ref shape_ref_is_Simplex).
 Qed.
 
-Definition ord_nvtx_Sd := cast_ord nnvtx_eq_S_dd.
-Definition ord_Sd_nvtx := cast_ord (eq_sym nnvtx_eq_S_dd).
-
-Local Definition vtx_ref : '('R^dd)^nnvtx := 
-   fun i:'I_nnvtx => vtx FE_ref (ord_Sd_nvtx i).
+Local Definition vtx_ref : '('R^dd)^nnvtx := castF nnvtx_eq_S_dd (vtx FE_ref).
 
 Lemma P_approx_ref_zero : P_approx_ref zero.
 Proof.
@@ -106,17 +102,9 @@ Qed.
 
 Local Definition K_geom_ref : 'R^dd -> Prop := convex_envelop vtx_ref.
 
-(* Pas besoin de ce lemme *)
 Lemma K_geom_ref_def_correct : K_geom_ref = K_geom FE_ref.
 Proof.
-(* simplifier la preuve *)
-apply fun_ext.
-intros x; unfold K_geom_ref, K_geom; unfold vtx_ref.
-apply prop_ext; split.
-eapply convex_envelop_cast with (H:=eq_sym nnvtx_eq_S_dd); intros i; f_equal;
-   apply ord_inj; easy.
-eapply convex_envelop_cast with (H:=nnvtx_eq_S_dd); intros i; f_equal;
-   apply ord_inj; easy.
+apply eq_sym, (convex_envelop_castF nnvtx_eq_S_dd); easy.
 Qed.
 
 (* FE_ref is indeed a reference FE *)
@@ -296,14 +284,14 @@ simpl; unfold gather, swap; simpl; easy.
 Qed.
 
 Definition FE_cur :=
-  mk_FE dd nndof dd_pos nndof_pos shape_ref 
-  (fun i => vtx_cur (ord_nvtx_Sd i))
+  mk_FE dd nndof dd_pos nndof_pos shape_ref
+  (castF (eq_sym nnvtx_eq_S_dd) vtx_cur)
   P_approx_cur P_approx_cur_compat_fin Sigma_cur
   Sigma_cur_lin_map unisolvence_cur.
 
 Definition d_cur := d FE_cur.
 
-Definition ndof_cur := ndof FE_cur. 
+Definition ndof_cur := ndof FE_cur.
 
 Definition shape_fun_cur : '(FRd d_cur)^ndof_cur := shape_fun FE_cur.
 
@@ -315,18 +303,7 @@ Qed.
 
 Lemma K_geom_cur_def_correct : K_geom_cur = K_geom FE_cur.
 Proof.
-assert (H:nnvtx = nvtx FE_cur).
-rewrite nvtx_cur_eq; easy.
-apply fun_ext.
-intros x; unfold K_geom_cur, K_geom.
-replace (vtx FE_cur) with (fun i => vtx_cur (ord_nvtx_Sd i)).
-2: apply fun_ext; unfold FE_cur; simpl; easy.
-apply prop_ext; split.
-eapply convex_envelop_cast with (H:=H).
-intros i; f_equal; apply ord_inj; easy.
-apply eq_sym in H.
-eapply convex_envelop_cast with (H:=H).
-intros i; f_equal; apply ord_inj; easy.
+apply (convex_envelop_castF (eq_sym nnvtx_eq_S_dd)); easy.
 Qed.
 
 Lemma P_approx_ref_image : 
diff --git a/FEM/geometry.v b/FEM/geometry.v
index d297cef9edaa5293702f48f5b7bcf985c7267ab9..c7088933ffb67cdcb335a34c405e7f1081d4cadb 100644
--- a/FEM/geometry.v
+++ b/FEM/geometry.v
@@ -22,6 +22,8 @@ Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat fintype.
 Set Warnings "notation-overridden".
 
+From Lebesgue Require Import Subset.
+
 From FEM Require Import Algebra.
 
 Local Open Scope R_scope.
@@ -92,24 +94,25 @@ Section Geometry_2.
 
 Context {E : ModuleSpace R_Ring}.
 
-Lemma convex_envelop_cast:
-  forall { n m : nat} (H:n=m) (v1:'E^n) (v2:'E^m) x,
-    (forall i, v1 i = v2 (cast_ord H i)) ->
-    convex_envelop v1 x -> convex_envelop v2 x.
+Lemma convex_envelop_castF_incl :
+  forall {n1 n2} (H : n1 = n2) (v1 : 'E^n1) (v2 : 'E^n2),
+    v2 = castF H v1 -> incl (convex_envelop v1) (convex_envelop v2).
+Proof.
+intros n1 n2 Hn v1 v2 Hv _ [L1 HL1a HL1b].
+apply convex_envelop_correct; exists (castF Hn L1); repeat split.
+unfold castF; easy.
+rewrite sum_castF; easy.
+rewrite Hv; apply eq_sym, comb_lin_castF.
+Qed.
+
+Lemma convex_envelop_castF :
+  forall {n1 n2} (H : n1 = n2) (v1 : 'E^n1) (v2 : 'E^n2),
+    v2 = castF H v1 -> convex_envelop v1 = convex_envelop v2.
 Proof.
-intros n m H v1 v2 x H1 H2.
-(*assert (H': m=n) by easy.*)
-apply convex_envelop_correct in H2.
-destruct H2 as [L [HL1 [HL2 HL3]]].
-apply convex_envelop_correct.
-unfold convex_envelop_ex.
-exists (castF H L).
-split; try now unfold castF.
-split.
-rewrite <- HL2 at 1.
-rewrite <- (sum_castF H); easy.
-rewrite HL3 -(comb_lin_castF H); f_equal.
-apply extF; intro; unfold castF; rewrite -> H1, cast_ordKV; easy.
+intros; apply subset_ext_equiv; split.
+apply (convex_envelop_castF_incl H); easy.
+apply (convex_envelop_castF_incl (eq_sym H)).
+subst; rewrite castF_can; easy.
 Qed.
 
 End Geometry_2.