From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 26 Jul 2016 18:50:33 +0000 (+0000)
Subject: bug fix in the context reduction rule for cast (cpm)
X-Git-Tag: make_still_working~545
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=138e01310a2334cd531819122c794d72d14c6e8c

bug fix in the context reduction rule for cast (cpm)
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_6.ma
deleted file mode 100644
index 096a26e4c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_6.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 c , break term 46 h ] break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'PRedTy $c $h $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma
new file mode 100644
index 000000000..291bf9075
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 Rt , break term 46 c , break term 46 h ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedTy $Rt $c $h $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
index e322f490f..c704ddf6b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -14,7 +14,7 @@
 
 include "ground_2/steps/rtc_max.ma".
 include "ground_2/steps/rtc_plus.ma".
-include "basic_2/notation/relations/predty_6.ma".
+include "basic_2/notation/relations/predty_7.ma".
 include "basic_2/grammar/lenv.ma".
 include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/lifts.ma".
@@ -23,69 +23,69 @@ include "basic_2/static/sh.ma".
 (* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
 
 (* avtivate genv *)
-inductive cpg (h): rtc → relation4 genv lenv term term ≝
-| cpg_atom : ∀I,G,L. cpg h (𝟘𝟘) G L (⓪{I}) (⓪{I})
-| cpg_ess  : ∀G,L,s. cpg h (𝟘𝟙) G L (⋆s) (⋆(next h s))
-| cpg_delta: ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
-             ⬆*[1] V2 ≡ W2 → cpg h c G (L.ⓓV1) (#0) W2
-| cpg_ell  : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
-             ⬆*[1] V2 ≡ W2 → cpg h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2
-| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T → 
-             ⬆*[1] T ≡ U → cpg h c G (L.ⓑ{I}V) (#⫯i) U
+inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝
+| cpg_atom : ∀I,G,L. cpg Rt h (𝟘𝟘) G L (⓪{I}) (⓪{I})
+| cpg_ess  : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(next h s))
+| cpg_delta: ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
+             ⬆*[1] V2 ≡ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2
+| cpg_ell  : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
+             ⬆*[1] V2 ≡ W2 → cpg Rt h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2
+| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg Rt h c G L (#i) T → 
+             ⬆*[1] T ≡ U → cpg Rt h c G (L.ⓑ{I}V) (#⫯i) U
 | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2.
-             cpg h cV G L V1 V2 → cpg h cT G (L.ⓑ{I}V1) T1 T2 →
-             cpg h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
-| cpg_flat : ∀cV,cT,I,G,L,V1,V2,T1,T2.
-             cpg h cV G L V1 V2 → cpg h cT G L T1 T2 →
-             cpg h ((↓cV)∨cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg h c G (L.ⓓV) T1 T →
-             ⬆*[1] T2 ≡ T → cpg h (c+𝟙𝟘) G L (+ⓓV.T1) T2
-| cpg_eps  : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h (c+𝟙𝟘) G L (ⓝV.T1) T2
-| cpg_ee   : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h (c+𝟘𝟙) G L (ⓝV1.T) V2
+             cpg Rt h cV G L V1 V2 → cpg Rt h cT G (L.ⓑ{I}V1) T1 T2 →
+             cpg Rt h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+| cpg_appl : ∀cV,cT,G,L,V1,V2,T1,T2.
+             cpg Rt h cV G L V1 V2 → cpg Rt h cT G L T1 T2 →
+             cpg Rt h ((↓cV)∨cT) G L (ⓐV1.T1) (ⓐV2.T2)
+| cpg_cast : ∀cU,cT,G,L,U1,U2,T1,T2. Rt cU cT →
+             cpg Rt h cU G L U1 U2 → cpg Rt h cT G L T1 T2 →
+             cpg Rt h (cU∨cT) G L (ⓝU1.T1) (ⓝU2.T2)
+| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg Rt h c G (L.ⓓV) T1 T →
+             ⬆*[1] T2 ≡ T → cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2
+| cpg_eps  : ∀c,G,L,V,T1,T2. cpg Rt h c G L T1 T2 → cpg Rt h (c+𝟙𝟘) G L (ⓝV.T1) T2
+| cpg_ee   : ∀c,G,L,V1,V2,T. cpg Rt h c G L V1 V2 → cpg Rt h (c+𝟘𝟙) G L (ⓝV1.T) V2
 | cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2.
-             cpg h cV G L V1 V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓛW1) T1 T2 →
-             cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+             cpg Rt h cV G L V1 V2 → cpg Rt h cW G L W1 W2 → cpg Rt h cT G (L.ⓛW1) T1 T2 →
+             cpg Rt h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
 | cpg_theta: ∀cV,cW,cT,p,G,L,V1,V,V2,W1,W2,T1,T2.
-             cpg h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg h cW G L W1 W2 →
-             cpg h cT G (L.ⓓW1) T1 T2 →
-             cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+             cpg Rt h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg Rt h cW G L W1 W2 →
+             cpg Rt h cT G (L.ⓓW1) T1 T2 →
+             cpg Rt h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
 .
 
 interpretation
    "counted context-sensitive parallel rt-transition (term)"
-   'PRedTy c h G L T1 T2 = (cpg h c G L T1 T2).
+   'PRedTy Rt c h G L T1 T2 = (cpg Rt h c G L T1 T2).
 
 (* Basic properties *********************************************************)
 
-(* Note: this is "∀h,g,L. reflexive … (cpg h (𝟘𝟘) L)" *)
-lemma cpg_refl: ∀h,G,T,L. ⦃G, L⦄ ⊢ T ⬈[𝟘𝟘, h] T.
-#h #G #T elim T -T // * /2 width=1 by cpg_bind, cpg_flat/
-qed.
-
-lemma cpg_pair_sn: ∀c,h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[c, h] V2 →
-                   ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈[↓c, h] ②{I}V2.T.
-#c #h * /2 width=1 by cpg_bind, cpg_flat/
+(* Note: this is "∀Rt. reflexive … Rt → ∀h,g,L. reflexive … (cpg Rt h (𝟘𝟘) L)" *)
+lemma cpg_refl: ∀Rt. reflexive … Rt → ∀h,G,T,L. ⦃G, L⦄ ⊢ T ⬈[Rt, 𝟘𝟘, h] T.
+#Rt #HRt #h #G #T elim T -T // * /2 width=1 by cpg_bind/
+* /2 width=1 by cpg_appl, cpg_cast/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2 → ∀J. T1 = ⓪{J} →
+fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[Rt, c, h] T2 → ∀J. T1 = ⓪{J} →
                         ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                          | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
-                         | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                         | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓓV1 & J = LRef 0 & c = cV
-                         | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                         | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙
-                         | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 &
+                         | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 &
                                         L = K.ⓑ{I}V & J = LRef (⫯i).
-#c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
+#Rt #c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
 [ #I #G #L #J #H destruct /3 width=1 by or5_intro0, conj/
 | #G #L #s #J #H destruct /3 width=3 by or5_intro1, ex3_intro/
 | #c #G #L #V1 #V2 #W2 #HV12 #VW2 #J #H destruct /3 width=8 by or5_intro2, ex5_4_intro/
 | #c #G #L #V1 #V2 #W2 #HV12 #VW2 #J #H destruct /3 width=8 by or5_intro3, ex5_4_intro/
 | #c #I #G #L #V #T #U #i #HT #HTU #J #H destruct /3 width=9 by or5_intro4, ex4_5_intro/
 | #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
-| #cV #cT #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #cU #cT #G #L #U1 #U2 #T1 #T2 #_ #_ #_ #J #H destruct
 | #c #G #L #V #T1 #T #T2 #_ #_ #J #H destruct
 | #c #G #L #V #T1 #T2 #_ #J #H destruct
 | #c #G #L #V1 #V2 #T #_ #J #H destruct
@@ -94,20 +94,20 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2 → ∀
 ]
 qed-.
 
-lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[c, h] T2 →
+lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[Rt, c, h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                       | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
-                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓓV1 & J = LRef 0 & c = cV
-                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙
-                      | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 &
+                      | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 &
                                      L = K.ⓑ{I}V & J = LRef (⫯i).
 /2 width=3 by cpg_inv_atom1_aux/ qed-.
 
-lemma cpg_inv_sort1: ∀c,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[c, h] T2 →
+lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[Rt, c, h] T2 →
                      (T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙).
-#c #h #G #L #T2 #s #H
+#Rt #c #h #G #L #T2 #s #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 [ #s0 #H destruct /3 width=1 by or_intror, conj/
 |2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
@@ -115,13 +115,13 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 ]
 qed-.
 
-lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[c, h] T2 →
+lemma cpg_inv_zero1: ∀Rt,c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[Rt, c, h] T2 →
                      ∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
-                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓓV1 & c = cV
-                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & c = cV+𝟘𝟙.
-#c #h #G #L #T2 #H
+#Rt #c #h #G #L #T2 #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
 [ #s #H destruct
 |2,3: #cV #K #V1 #V2 #HV12 #HVT2 #H1 #_ #H2 destruct /3 width=8 by or3_intro1, or3_intro2, ex4_4_intro/
@@ -129,10 +129,10 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
 ]
 qed-.
 
-lemma cpg_inv_lref1: ∀c,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[c, h] T2 →
+lemma cpg_inv_lref1: ∀Rt,c,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 →
                      (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
-                     ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
-#c #h #G #L #T2 #i #H
+                     ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+#Rt #c #h #G #L #T2 #i #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 [ #s #H destruct
 |2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
@@ -140,8 +140,8 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 ]
 qed-.
 
-lemma cpg_inv_gref1: ∀c,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
-#c #h #G #L #T2 #l #H
+lemma cpg_inv_gref1: ∀Rt,c,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[Rt, c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
+#Rt #c #h #G #L #T2 #l #H
 elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
 [ #s #H destruct
 |2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
@@ -149,127 +149,127 @@ elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
 ]
 qed-.
 
-fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
+fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
                         ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
-                        ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[cT, h] T2 &
+                        ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
                                        U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT)
                         ) ∨
-                        ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+                        ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
                                 p = true & J = Abbr & c = cT+𝟙𝟘.
-#c #h #G #L #U #U2 * -c -G -L -U -U2
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
 [ #I #G #L #q #J #W #U1 #H destruct
 | #G #L #s #q #J #W #U1 #H destruct
 | #c #G #L #V1 #V2 #W2 #_ #_ #q #J #W #U1 #H destruct
 | #c #G #L #V1 #V2 #W2 #_ #_ #q #J #W #U1 #H destruct
 | #c #I #G #L #V #T #U #i #_ #_ #q #J #W #U1 #H destruct
-| #rv #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W #U1 #H destruct /3 width=8 by ex4_4_intro, or_introl/
-| #rv #cT #I #G #L #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W #U1 #H destruct /3 width=8 by ex4_4_intro, or_introl/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
+| #cU #cT #G #L #U1 #U2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
 | #c #G #L #V #T1 #T #T2 #HT1 #HT2 #q #J #W #U1 #H destruct /3 width=5 by ex5_2_intro, or_intror/
 | #c #G #L #V #T1 #T2 #_ #q #J #W #U1 #H destruct
 | #c #G #L #V1 #V2 #T #_ #q #J #W #U1 #H destruct
-| #rv #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
-| #rv #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #q #J #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #q #J #W #U1 #H destruct
 ]
 qed-.
 
-lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] U2 → (
-                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 → (
+                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                     U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT)
                      ) ∨
-                     ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+                     ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
                              p = true & I = Abbr & c = cT+𝟙𝟘.
 /2 width=3 by cpg_inv_bind1_aux/ qed-.
 
-lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 → (
-                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 → (
+                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                     U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT)
                      ) ∨
-                     ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+                     ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
                              p = true & c = cT+𝟙𝟘.
-#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
+#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
 /3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
 qed-.
 
-lemma cpg_inv_abst1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[c, h] U2 →
-                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_abst1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[Rt, c, h] U2 →
+                     ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                     U2 = ⓛ{p}V2.T2 & c = ((↓cV)∨cT).
-#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * 
+#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * 
 [ /3 width=8 by ex4_4_intro/
 | #c #T #_ #_ #_ #H destruct
 ]
 qed-.
 
-fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
-                        ∀J,V1,U1. U = ⓕ{J}V1.U1 →
-                        ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                          U2 = ⓕ{J}V2.T2 & c = ((↓cV)∨cT)
-                         | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = cT+𝟙𝟘
-                         | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = cV+𝟘𝟙
-                         | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                        J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
-                         | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                          J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-#c #h #G #L #U #U2 * -c -G -L -U -U2
-[ #I #G #L #J #W #U1 #H destruct
-| #G #L #s #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #I #G #L #V #T #U #i #_ #_ #J #W #U1 #H destruct
-| #rv #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #rv #cT #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=8 by or5_intro0, ex4_4_intro/
-| #c #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=3 by or5_intro1, ex3_intro/
-| #c #G #L #V1 #V2 #T #HV12 #J #W #U1 #H destruct /3 width=3 by or5_intro2, ex3_intro/
-| #rv #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=15 by or5_intro3, ex7_9_intro/
-| #rv #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=17 by or5_intro4, ex8_10_intro/
+fact cpg_inv_appl1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
+                        ∀V1,U1. U = ⓐV1.U1 →
+                        ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+                                          U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
+                         | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+                                                        U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
+                         | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+                                                          U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
+[ #I #G #L #W #U1 #H destruct
+| #G #L #s #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #I #G #L #V #T #U #i #_ #_ #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #W #U1 #H destruct /3 width=8 by or3_intro0, ex4_4_intro/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T #T2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T2 #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #T #_ #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #W #U1 #H destruct /3 width=15 by or3_intro1, ex6_9_intro/
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #W #U1 #H destruct /3 width=17 by or3_intro2, ex7_10_intro/
 ]
 qed-.
 
-lemma cpg_inv_flat1: ∀c,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[c, h] U2 →
-                     ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓕ{I}V2.T2 & c = ((↓cV)∨cT)
-                      | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = cT+𝟙𝟘
-                      | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = cV+𝟘𝟙
-                      | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                     I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
-                      | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                       I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-/2 width=3 by cpg_inv_flat1_aux/ qed-.
-
-lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[c, h] U2 →
-                     ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
+lemma cpg_inv_appl1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[Rt, c, h] U2 →
+                     ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
                                        U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
-                      | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
+                      | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                                      U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
-                      | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
+                      | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                                        U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
-[ /3 width=8 by or3_intro0, ex4_4_intro/
-|2,3: #c #_ #H destruct
-| /3 width=15 by or3_intro1, ex6_9_intro/
-| /3 width=17 by or3_intro2, ex7_10_intro/
-]
-qed-.
+/2 width=3 by cpg_inv_appl1_aux/ qed-.
 
-lemma cpg_inv_cast1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[c, h] U2 →
-                     ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓝV2.T2 & c = ((↓cV)∨cT)
-                      | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = cT+𝟙𝟘
-                      | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = cV+𝟘𝟙.
-#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
-[ /3 width=8 by or3_intro0, ex4_4_intro/
-|2,3: /3 width=3 by or3_intro1, or3_intro2, ex2_intro/
-| #rv #cW #cT #p #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #H destruct
-| #rv #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #H destruct
+fact cpg_inv_cast1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
+                        ∀V1,U1. U = ⓝV1.U1 →
+                        ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+                                          Rt cV cT & U2 = ⓝV2.T2 & c = (cV∨cT)
+                         | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] U2 & c = cT+𝟙𝟘
+                         | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙.
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
+[ #I #G #L #W #U1 #H destruct
+| #G #L #s #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #I #G #L #V #T #U #i #_ #_ #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HRt #HV12 #HT12 #W #U1 #H destruct /3 width=9 by or3_intro0, ex5_4_intro/
+| #c #G #L #V #T1 #T #T2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T2 #HT12 #W #U1 #H destruct /3 width=3 by or3_intro1, ex2_intro/
+| #c #G #L #V1 #V2 #T #HV12 #W #U1 #H destruct /3 width=3 by or3_intro2, ex2_intro/
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #W #U1 #H destruct
 ]
 qed-.
 
+lemma cpg_inv_cast1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[Rt, c, h] U2 →
+                     ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+                                       Rt cV cT & U2 = ⓝV2.T2 & c = (cV∨cT)
+                      | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] U2 & c = cT+𝟙𝟘
+                      | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙.
+/2 width=3 by cpg_inv_cast1_aux/ qed-.
+
 (* Basic forward lemmas *****************************************************)
 
-lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[c, h] T → ∀p.
-                           ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] ⓑ{p,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: ∀Rt,c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[Rt, c, h] T → ∀p.
+                           ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] ⓑ{p,I}V2.T2 &
                                     T = -ⓑ{I}V2.T2.
-#c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
+#Rt #c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/
 | #c #T2 #_ #_ #H destruct
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
index b22fc0938..6c9fdfd22 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
@@ -21,9 +21,9 @@ include "basic_2/rt_transition/cpg.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma cpg_delta_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ⬈[c, h] V2 →
-                       ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ⬈[c, h] T2.
-#c #h #G #K #V #V2 #i elim i -i
+lemma cpg_delta_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ⬈[Rt, c, h] V2 →
+                       ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ⬈[Rt, c, h] T2.
+#Rt #c #h #G #K #V #V2 #i elim i -i
 [ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_delta/
 | #i #IH #L0 #T0 #H0 #HV2 #HVT2
   elim (drops_inv_succ … H0) -H0 #I #L #V0 #HLK #H destruct
@@ -31,9 +31,9 @@ lemma cpg_delta_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K
 ]
 qed.
 
-lemma cpg_ell_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ⬈[c, h] V2 →
-                     ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ⬈[c+𝟘𝟙, h] T2.
-#c #h #G #K #V #V2 #i elim i -i
+lemma cpg_ell_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ⬈[Rt,c, h] V2 →
+                     ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ⬈[Rt, c+𝟘𝟙, h] T2.
+#Rt #c #h #G #K #V #V2 #i elim i -i
 [ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_ell/
 | #i #IH #L0 #T0 #H0 #HV2 #HVT2
   elim (drops_inv_succ … H0) -H0 #I #L #V0 #HLK #H destruct
@@ -43,13 +43,13 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[c, h] T2 →
+lemma cpg_inv_lref1_drops: ∀Rt,c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[Rt,c, h] T2 →
                            ∨∨ T2 = #i ∧ c = 𝟘𝟘
-                            | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+                            | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
                                            ⬆*[⫯i] V2 ≡ T2 & c = cV
-                            | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+                            | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
                                            ⬆*[⫯i] V2 ≡ T2 & c = cV + 𝟘𝟙.
-#c #h #G #i elim i -i
+#Rt #c #h #G #i elim i -i
 [ #L #T2 #H elim (cpg_inv_zero1 … H) -H * /3 width=1 by or3_intro0, conj/
   /4 width=8 by drops_refl, ex4_4_intro, or3_intro2, or3_intro1/
 | #i #IH #L #T2 #H elim (cpg_inv_lref1 … H) -H * /3 width=1 by or3_intro0, conj/
@@ -61,14 +61,14 @@ lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[c, h] T2 →
 ]
 qed-.
 
-lemma cpg_inv_atom1_drops: ∀c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[c, h] T2 →
+lemma cpg_inv_atom1_drops: ∀Rt,c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[Rt, c, h] T2 →
                            ∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘
                             | ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙
-                            | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+                            | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
                                              ⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV
-                            | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+                            | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
                                              ⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV + 𝟘𝟙.
-#c #h * #n #G #L #T2 #H
+#Rt #c #h * #n #G #L #T2 #H
 [ elim (cpg_inv_sort1 … H) -H *
   /3 width=3 by or4_intro0, or4_intro1, ex3_intro, conj/
 | elim (cpg_inv_lref1_drops … H) -H *
@@ -81,8 +81,8 @@ qed-.
 (* Properties with generic slicing for local environments *******************)
 
 (* Note: it should use drops_split_trans_pair2 *)
-lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G).
-#c #h #G #K #T generalize in match c; -c
+lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G).
+#Rt #HRt #c #h #G #K #T generalize in match c; -c
 @(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * *
 [ #s #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct -IH
   lapply (lifts_inv_sort1 … H1) -H1 #H destruct
@@ -90,7 +90,7 @@ lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G).
   /2 width=3 by cpg_atom, cpg_ess, lifts_sort, ex2_intro/
 | #i1 #HG #HK #HT #c #T2 #H2 #b #f #L #HLK #X1 #H1 destruct
   elim (cpg_inv_lref1_drops … H2) -H2 *
-  [ #H1 #H2 destruct /2 width=3 by ex2_intro/ ]
+  [ #H1 #H2 destruct /3 width=3 by cpg_refl, ex2_intro/ ]
   #cV #K0 #V #V2 #HK0 #HV2 #HVT2 #H destruct
   elim (lifts_inv_lref1 … H1) -H1 #i2 #Hf #H destruct
   lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H
@@ -119,42 +119,49 @@ lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G).
     elim (lifts_split_trans … HXU2 f (𝐔❴⫯O❵)) [2: /2 width=1 by after_uni_one_dx/ ]
     /3 width=5 by cpg_zeta, ex2_intro/
   ]
-| #I #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct
+| * #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct
   elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #HVW1 #HTU1 #H destruct
-  elim (cpg_inv_flat1 … H2) -H2 *
-  [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-    elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
-    elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
-    /3 width=5 by cpg_flat, lifts_flat, ex2_intro/
-  | #cT #HT12 #H1 #H2 destruct
-    elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
-    /3 width=3 by cpg_eps, ex2_intro/
-  | #cV #HV12 #H1 #H2 destruct
-    elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
-    /3 width=3 by cpg_ee, ex2_intro/
-  | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
-    elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
-    elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
-    elim (IH … HY12 … HLK … HYZ1) -HY12 //
-    elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
-    /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
-  | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
-    elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
-    elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
-    elim (IH … HY12 … HLK … HYZ1) -HY12 //
-    elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
-    elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
-    lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
-    lapply (lifts_conf … HV20 … H (↑f) ?) -V2 /2 width=3 by after_uni_one_sn/
-    /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+  [ elim (cpg_inv_appl1 … H2) -H2 *
+    [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+      elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+      elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+      /3 width=5 by cpg_appl, lifts_flat, ex2_intro/
+    | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 destruct
+      elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+      elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+      elim (IH … HY12 … HLK … HYZ1) -HY12 //
+      elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+      /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
+    | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 destruct
+      elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+      elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
+      elim (IH … HY12 … HLK … HYZ1) -HY12 //
+      elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+      elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
+      lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
+      lapply (lifts_conf … HV20 … H (↑f) ?) -V2 /2 width=3 by after_uni_one_sn/
+      /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+    ]
+  | elim (cpg_inv_cast1 … H2) -H2 *
+    [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
+      elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+      elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+      /3 width=5 by cpg_cast, lifts_flat, ex2_intro/
+    | #cT #HT12 #H destruct
+      elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+      /3 width=3 by cpg_eps, ex2_intro/
+    | #cV #HV12 #H destruct
+      elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
+      /3 width=3 by cpg_ee, ex2_intro/
+    ]
   ]
 ]
 qed-.
 
 (* Inversion lemmas with generic slicing for local environments *************)
 
-lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G).
-#c #h #G #L #U generalize in match c; -c
+lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
+#Rt #HRt #c #h #G #L #U generalize in match c; -c
 @(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * *
 [ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH
   lapply (lifts_inv_sort2 … H1) -H1 #H destruct
@@ -162,7 +169,7 @@ lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G).
   /2 width=3 by cpg_atom, cpg_ess, lifts_sort, ex2_intro/
 | #i2 #HG #HL #HU #c #U2 #H2 #b #f #K #HLK #X1 #H1 destruct
   elim (cpg_inv_lref1_drops … H2) -H2 *
-  [ #H1 #H2 destruct /2 width=3 by ex2_intro/ ]
+  [ #H1 #H2 destruct /3 width=3 by cpg_refl, ex2_intro/ ]
   #cW #L0 #W #W2 #HL0 #HW2 #HWU2 #H destruct
   elim (lifts_inv_lref2 … H1) -H1 #i1 #Hf #H destruct
   lapply (drops_split_div … HLK (𝐔❴i1❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK0 #HLY0
@@ -188,33 +195,40 @@ lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G).
     elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ] #T2 #HTU2 #HT12
     elim (lifts_div4_one … HTU2 … HXU2) -U2 /3 width=5 by cpg_zeta, ex2_intro/
   ]
-| #I #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct
+| * #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct
   elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct
-  elim (cpg_inv_flat1 … H2) -H2 *
-  [ #cW #cU #W2 #U2 #HW12 #HU12 #H1 #H2 destruct
-    elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
-    elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
-    /3 width=5 by cpg_flat, lifts_flat, ex2_intro/
-  | #cU #HU12 #H1 #H2 destruct
-    elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
-    /3 width=3 by cpg_eps, ex2_intro/
-  | #cW #HW12 #H1 #H2 destruct
-    elim (IH … HW12 … HLK … HVW1) -IH -HW12 -HLK -HVW1 //
-    /3 width=3 by cpg_ee, ex2_intro/
-  | #cW #cZ #cU #a #W2 #Z1 #Z2 #U0 #U2 #HW12 #HZ12 #HU12 #H1 #H2 #H3 #H4 destruct
-    elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
-    elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
-    elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
-    elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
-    /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
-  | #cW #cZ #cU #a #W2 #W20 #Z1 #Z2 #U0 #U2 #HW12 #HW20 #HZ12 #HU12 #H1 #H2 #H3 #H4 destruct
-    elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
-    elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 // #V2 #HVW2 #HV12
-    elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
-    elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
-    lapply (lifts_trans … HVW2 … HW20 ??) -W2 [3: |*: // ] #H
-    elim (lifts_split_trans … H ? (↑f)) -H [ |*: /2 width=3 by after_uni_one_sn/ ]
-    /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+  [ elim (cpg_inv_appl1 … H2) -H2 *
+    [ #cW #cU #W2 #U2 #HW12 #HU12 #H1 #H2 destruct
+      elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+      elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+      /3 width=5 by cpg_appl, lifts_flat, ex2_intro/
+    | #cW #cZ #cU #a #W2 #Z1 #Z2 #U0 #U2 #HW12 #HZ12 #HU12 #H1 #H2 #H3 destruct
+      elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
+      elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+      elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
+      elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+      /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
+    | #cW #cZ #cU #a #W2 #W20 #Z1 #Z2 #U0 #U2 #HW12 #HW20 #HZ12 #HU12 #H1 #H2 #H3 destruct
+      elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
+      elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 // #V2 #HVW2 #HV12
+      elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
+      elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+      lapply (lifts_trans … HVW2 … HW20 ??) -W2 [3: |*: // ] #H
+      elim (lifts_split_trans … H ? (↑f)) -H [ |*: /2 width=3 by after_uni_one_sn/ ]
+      /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+    ]
+  | elim (cpg_inv_cast1 … H2) -H2 *
+    [ #cW #cU #W2 #U2 #HW12 #HU12 #HcWU #H1 #H2 destruct
+      elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+      elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+      /3 width=5 by cpg_cast, lifts_flat, ex2_intro/
+    | #cU #HU12 #H destruct
+      elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+      /3 width=3 by cpg_eps, ex2_intro/
+    | #cW #HW12 #H destruct
+      elim (IH … HW12 … HLK … HVW1) -IH -HW12 -HLK -HVW1 //
+      /3 width=3 by cpg_ee, ex2_intro/
+    ]
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
index 90f846e5a..8dcc523e4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
@@ -19,8 +19,8 @@ include "basic_2/rt_transition/cpg.ma".
 
 (* Properties with restricted refinement for local environments *************)
 
-lemma lsubr_cpg_trans: ∀c,h,G. lsub_trans … (cpg h c G) lsubr.
-#c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2
+lemma lsubr_cpg_trans: ∀Rt,c,h,G. lsub_trans … (cpg Rt h c G) lsubr.
+#Rt #c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2
 [ //
 | /2 width=2 by cpg_ess/
 | #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
@@ -32,8 +32,8 @@ lemma lsubr_cpg_trans: ∀c,h,G. lsub_trans … (cpg h c G) lsubr.
 | #c #I1 #G #L1 #V1 #T1 #U1 #i #_ #HTU1 #IH #X #H
   elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct
   /3 width=3 by cpg_lref/
-|6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
-|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ee/
-|8,12: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/
+|6,12: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
+|7,8,10,11: /3 width=1 by cpg_appl, cpg_cast, cpg_eps, cpg_ee/
+|9,13: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
index b03705a2e..0afd4cabb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
@@ -20,10 +20,10 @@ include "basic_2/rt_transition/cpg.ma".
 (* Properties with simple terms *********************************************)
 
 (* Note: the main property of simple terms *)
-lemma cpg_inv_appl1_simple: ∀c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[c, h] U → 𝐒⦃T1⦄ →
-                            ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_appl1_simple: ∀Rt,c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[Rt, c, h] U → 𝐒⦃T1⦄ →
+                            ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
                                            U = ⓐV2.T2 & c = ((↓cV)∨cT).
-#c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
+#Rt #c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
 [ /2 width=8 by ex4_4_intro/
 | #cV #cW #cT #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H destruct
   elim (simple_inv_bind … HT1)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index 870f93598..2ff07da04 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_transition/cpg.ma".
 
 (* Basic_2A1: includes: cpr *)
 definition cpm (n) (h): relation4 genv lenv term term ≝
-                        λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2.
+                        λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[eq_t, c, h] T2.
 
 interpretation
    "semi-counted context-sensitive parallel rt-transition (term)"
@@ -57,18 +57,22 @@ qed.
 lemma cpm_bind: ∀n,h,p,I,G,L,V1,V2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 →
                 ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2.
-#n #h #p #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
+#n #h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HcV #HV12 *
 /5 width=5 by cpg_bind, isrt_max_O1, isr_shift, ex2_intro/
 qed.
 
-(* Note: cpr_flat: does not hold in basic_1 *)
-(* Basic_1: includes: pr2_thin_dx *)
-(* Basic_2A1: includes: cpr_flat *)
-lemma cpm_flat: ∀n,h,I,G,L,V1,V2,T1,T2.
+lemma cpm_appl: ∀n,h,G,L,V1,V2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
-                ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[n, h] ⓕ{I}V2.T2.
-#n #h #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
-/5 width=5 by isrt_max_O1, isr_shift, cpg_flat, ex2_intro/
+                ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[n, h] ⓐV2.T2.
+#n #h #G #L #V1 #V2 #T1 #T2 * #cV #HcV #HV12 *
+/5 width=5 by isrt_max_O1, isr_shift, cpg_appl, ex2_intro/
+qed.
+
+lemma cpm_cast: ∀n,h,G,L,U1,U2,T1,T2.
+                ⦃G, L⦄ ⊢ U1 ➡[n, h] U2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
+                ⦃G, L⦄ ⊢ ⓝU1.T1 ➡[n, h] ⓝU2.T2.
+#n #h #G #L #U1 #U2 #T1 #T2 * #cU #HcU #HU12 *
+/4 width=6 by cpg_cast, isrt_max_idem1, isrt_mono, ex2_intro/
 qed.
 
 (* Basic_2A1: includes: cpr_zeta *)
@@ -111,14 +115,7 @@ qed.
 (* Basic_1: includes by definition: pr0_refl *)
 (* Basic_2A1: includes: cpr_atom *)
 lemma cpr_refl: ∀h,G,L. reflexive … (cpm 0 h G L).
-/2 width=3 by ex2_intro/ qed.
-
-(* Basic_1: was: pr2_head_1 *)
-lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
-                   ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T.
-#h #I #G #L #V1 #V2 *
-/3 width=3 by cpg_pair_sn, isr_shift, ex2_intro/
-qed.
+/3 width=3 by cpg_refl, ex2_intro/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -229,46 +226,6 @@ elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
 /3 width=5 by ex3_2_intro, ex2_intro/
 qed-.
 
-lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h] U2 →
-                     ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 &
-                                 U2 = ⓕ{I}V2.T2
-                      | (⦃G, L⦄ ⊢ U1 ➡[n, h] U2 ∧ I = Cast)
-                      | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & I = Cast & n = ⫯m
-                      | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ W1 ➡[h] W2 &
-                                            ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 &
-                                            U1 = ⓛ{p}W1.T1 &
-                                            U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
-                      | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V & ⬆*[1] V ≡ V2 &
-                                              ⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 &
-                                              U1 = ⓓ{p}W1.T1 &
-                                              U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#n #h #I #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_flat1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
-  elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
-  /4 width=5 by or5_intro0, ex3_2_intro, ex2_intro/
-| #cU #U12 #H1 #H2 destruct
-  /5 width=3 by isrt_inv_plus_O_dx, or5_intro1, conj, ex2_intro/
-| #cU #H12 #H1 #H2 destruct
-  elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct
-  /4 width=3 by or5_intro2, ex3_intro, ex2_intro/
-| #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
-  lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
-  elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
-  elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
-  /4 width=11 by or5_intro3, ex6_6_intro, ex2_intro/
-| #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
-  lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
-  elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
-  elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
-  /4 width=13 by or5_intro4, ex7_7_intro, ex2_intro/
-]
-qed-.
-
 (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
 (* Basic_2A1: includes: cpr_inv_appl1 *)
 lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 →
@@ -303,14 +260,15 @@ lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2
 qed-.
 
 lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 →
-                     ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n,h] T2 &
+                     ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 &
                                  U2 = ⓝV2.T2
                       | ⦃G, L⦄ ⊢ U1 ➡[n, h] U2
                       | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ⫯m.
 #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+[ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
   elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
-  elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
+  lapply (isrt_eq_t_trans … HcV HcVT) -HcVT #H
+  lapply (isrt_inj … H HcT) -H #H destruct <idempotent_max
   /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/
 | #cU #U12 #H destruct
   /4 width=3 by isrt_inv_plus_O_dx, or3_intro1, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
index 382bb119b..a5d3ca4d3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
@@ -16,6 +16,22 @@ include "basic_2/rt_transition/cpm.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
 
+(* Basic properties *********************************************************)
+
+(* Note: cpr_flat: does not hold in basic_1 *)
+(* Basic_1: includes: pr2_thin_dx *)
+lemma cpr_flat: ∀h,I,G,L,V1,V2,T1,T2.
+                ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
+                ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[h] ⓕ{I}V2.T2.
+#h * /2 width=1 by cpm_cast, cpm_appl/
+qed. 
+
+(* Basic_1: was: pr2_head_1 *)
+lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
+                   ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T.
+#h * /2 width=1 by cpm_bind, cpr_flat/
+qed.
+
 (* Basic inversion properties ***********************************************)
 
 lemma cpr_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h] T2 →
@@ -56,6 +72,15 @@ lemma cpr_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[h] T2 → T2 = §l.
 #h #G #L #T2 #l #H elim (cpm_inv_gref1 … H) -H //
 qed-.
 
+(* Basic_1: includes: pr0_gen_cast pr2_gen_cast *)
+lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡[h] U2 → (
+                     ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
+                              U2 = ⓝV2.T2
+                     ) ∨ ⦃G, L⦄ ⊢ U1 ➡[h] U2.
+#h #G #L #V1 #U1 #U2 #H elim (cpm_inv_cast1 … H) -H
+/2 width=1 by or_introl, or_intror/ * #n #_ #H destruct
+qed-.
+
 lemma cpr_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h] U2 →
                      ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
                                  U2 = ⓕ{I}V2.T2
@@ -67,18 +92,12 @@ lemma cpr_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h] U2 
                                               ⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 &
                                               U1 = ⓓ{p}W1.T1 &
                                               U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#h #I #G #L #V1 #U1 #U2 #H elim (cpm_inv_flat1 … H) -H *
-/3 width=13 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex7_7_intro, ex6_6_intro, ex3_2_intro, conj/
-#n #_ #_ #H destruct
-qed-.
-
-(* Basic_1: includes: pr0_gen_cast pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡[h] U2 → (
-                     ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
-                              U2 = ⓝV2.T2
-                     ) ∨ ⦃G, L⦄ ⊢ U1 ➡[h] U2.
-#h #G #L #V1 #U1 #U2 #H elim (cpm_inv_cast1 … H) -H
-/2 width=1 by or_introl, or_intror/ * #n #_ #H destruct
+#h * #G #L #V1 #U1 #U2 #H
+[ elim (cpm_inv_appl1 … H) -H *
+  /3 width=13 by or4_intro0, or4_intro2, or4_intro3, ex7_7_intro, ex6_6_intro, ex3_2_intro/
+| elim (cpr_inv_cast1 … H) -H [ * ]
+  /3 width=5 by or4_intro0, or4_intro1, ex3_2_intro, conj/
+]
 qed-.
 
 (* Basic_1: removed theorems 12:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index 9900e8bf1..49652d10c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -18,7 +18,7 @@ include "basic_2/rt_transition/cpg.ma".
 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
 
 definition cpx (h): relation4 genv lenv term term ≝
-                    λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2.
+                    λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[eq_f, c, h] T2.
 
 interpretation
    "uncounted context-sensitive parallel rt-transition (term)"
@@ -52,8 +52,8 @@ qed.
 lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
                 ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
-#h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
-/3 width=2 by cpg_flat, ex_intro/
+#h * #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
+/3 width=5 by cpg_appl, cpg_cast, ex_intro/
 qed.
 
 lemma cpx_zeta: ∀h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T →
@@ -90,12 +90,13 @@ qed.
 
 (* Basic_2A1: includes: cpx_atom *)
 lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
-/2 width=2 by ex_intro/ qed.
+/3 width=2 by cpg_refl, ex_intro/ qed.
+
+(* Advanced properties ******************************************************)
 
 lemma cpx_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
                    ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈[h] ②{I}V2.T.
-#h #I #G #L #V1 #V2 *
-/3 width=2 by cpg_pair_sn, ex_intro/
+#h * /2 width=2 by cpx_flat, cpx_bind/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -162,23 +163,6 @@ lemma cpx_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[h] U2 
 /3 width=5 by ex3_2_intro, ex_intro/
 qed-.
 
-lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 →
-                     ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
-                                 U2 = ⓕ{I}V2.T2
-                      | (⦃G, L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
-                      | (⦃G, L⦄ ⊢ V1 ⬈[h] U2 ∧ I = Cast)
-                      | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[h] W2 &
-                                            ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 &
-                                            U1 = ⓛ{p}W1.T1 &
-                                            U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
-                      | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V & ⬆*[1] V ≡ V2 &
-                                              ⦃G, L⦄ ⊢ W1 ⬈[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 &
-                                              U1 = ⓓ{p}W1.T1 &
-                                              U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#h #I #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_flat1 … H) -H *
-/4 width=14 by or5_intro0, or5_intro1, or5_intro2, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro, ex_intro, conj/
-qed-.
-
 lemma cpx_inv_appl1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ⬈[h] U2 →
                      ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
                                  U2 = ⓐV2.T2
@@ -201,6 +185,29 @@ lemma cpx_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[h] U2 →
 /4 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex_intro/
 qed-.
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 →
+                     ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
+                                 U2 = ⓕ{I}V2.T2
+                      | (⦃G, L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
+                      | (⦃G, L⦄ ⊢ V1 ⬈[h] U2 ∧ I = Cast)
+                      | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[h] W2 &
+                                            ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 &
+                                            U1 = ⓛ{p}W1.T1 &
+                                            U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
+                      | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V & ⬆*[1] V ≡ V2 &
+                                              ⦃G, L⦄ ⊢ W1 ⬈[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 &
+                                              U1 = ⓓ{p}W1.T1 &
+                                              U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
+#h * #G #L #V1 #U1 #U2 #H
+[ elim (cpx_inv_appl1 … H) -H *
+  /3 width=14 by or5_intro0, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro/
+| elim (cpx_inv_cast1 … H) -H [ * ]
+  /3 width=14 by or5_intro0, or5_intro1, or5_intro2, ex3_2_intro, conj/
+] 
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma cpx_fwd_bind1_minus: ∀h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[h] T → ∀p.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
index 62228d229..87c091b19 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
@@ -38,3 +38,29 @@ interpretation "one r-step (rtc)"
 
 interpretation "one t-step (rtc)"
    'ZeroOne = (mk_rtc O O O (S O)).
+
+definition eq_f: relation rtc ≝ λc1,c2. ⊤.
+
+inductive eq_t: relation rtc ≝
+| eq_t_intro: ∀ri1,ri2,rs1,rs2,ti,ts.
+              eq_t (〈ri1, rs1, ti, ts〉) (〈ri2, rs2, ti, ts〉)
+.
+
+(* Basic properties *********************************************************)
+
+lemma eq_t_refl: reflexive …  eq_t.
+* // qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact eq_t_inv_dx_aux: ∀x,y. eq_t x y →
+                      ∀ri1,rs1,ti,ts. x = 〈ri1,rs1,ti,ts〉 →
+                      ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
+#x #y * -x -y
+#ri1 #ri #rs1 #rs #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H destruct -ri2 -rs2
+/2 width=3 by ex1_2_intro/
+qed-.
+
+lemma eq_t_inv_dx: ∀ri1,rs1,ti,ts,y. eq_t (〈ri1,rs1,ti,ts〉) y →
+                   ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
+/2 width=5 by eq_t_inv_dx_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma
index ced83577a..9c988abea 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma
@@ -34,6 +34,11 @@ lemma isr_10: 𝐑𝐓⦃0, 𝟙𝟘⦄.
 lemma isrt_01: 𝐑𝐓⦃1, 𝟘𝟙⦄.
 /2 width=3 by ex1_2_intro/ qed.
 
+lemma isrt_eq_t_trans: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → eq_t c1 c2 → 𝐑𝐓⦃n, c2⦄.
+#n #c1 #c2 * #ri1 #rs1 #H destruct
+#H elim (eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
+qed-.
+
 (* Basic inversion properties ***********************************************)
 
 lemma isrt_inv_00: ∀n. 𝐑𝐓⦃n, 𝟘𝟘⦄ → 0 = n.
@@ -50,6 +55,10 @@ qed-.
 
 (* Main inversion properties ************************************************)
 
-theorem isrt_mono: ∀n1,n2,c. 𝐑𝐓⦃n1, c⦄ → 𝐑𝐓⦃n2, c⦄ → n1 = n2.
+theorem isrt_inj: ∀n1,n2,c. 𝐑𝐓⦃n1, c⦄ → 𝐑𝐓⦃n2, c⦄ → n1 = n2.
 #n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
 qed-.
+
+theorem isrt_mono: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃n, c2⦄ → eq_t c1 c2.
+#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
index 46f457536..471f2d6ba 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
@@ -71,6 +71,10 @@ lemma isrt_max_O2: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃0, c2⦄ → 
 #n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by isrt_max/
 qed.
 
+lemma isrt_max_idem1: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃n, c2⦄ → 𝐑𝐓⦃n, c1∨c2⦄.
+#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by isrt_max/
+qed.
+
 (* Inversion properties with test for constrained rt-transition counter *****)
 
 lemma isrt_inv_max: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ →
@@ -83,7 +87,7 @@ qed-.
 lemma isrt_inv_max_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
 #n #c1 #c2 #H #H2
 elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct //
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
 qed-.
 
 (* Properties with shift ****************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
index b0b529240..ad9a04f01 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -83,13 +83,13 @@ qed-.
 lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
 #n #c1 #c2 #H #H2
 elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct //
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
 qed-.
 
 lemma isrt_inv_plus_SO_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃1, c2⦄ →
                            ∃∃m. 𝐑𝐓⦃m, c1⦄ & n = ⫯m.
 #n #c1 #c2 #H #H2
 elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct
 /2 width=3 by ex2_intro/
 qed-.