- notational change for cpg and cpx

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpg.ma

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 5dab2812e3d6bc5c4945551f446b6fcce8698787..b8742090c50969394388b66b35774e5d821358f2 100644 (file)
--- 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_shift.ma".
 include "ground_2/steps/rtc_plus.ma".
-include "basic_2/notation/relations/pred_6.ma".
+include "basic_2/notation/relations/predty_6.ma".
 include "basic_2/grammar/lenv.ma".
 include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/lifts.ma".
@@ -53,30 +53,30 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
 
 interpretation
    "counted context-sensitive parallel rt-transition (term)"
-   'PRed c h G L T1 T2 = (cpg h c G L T1 T2).
+   'PRedTy c h G L T1 T2 = (cpg h c G L T1 T2).
 
 (* Basic properties *********************************************************)
 
 (* Note: this is "∀h,g,L. reflexive … (cpg h (𝟘𝟘) L)" *)
-lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[𝟘𝟘, h] T.
+lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[𝟘𝟘, h] T.
 #h #G #T elim T -T // * /2 width=1 by cpg_bind, cpg_flat/
 qed.
 
-lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[c, h] V2 →
-                   â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â\9e¡[↓c, h] ②{I}V2.T.
+lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[c, h] V2 →
+                   â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â¬\88[↓c, h] ②{I}V2.T.
 #c #h * /2 width=1 by cpg_bind, cpg_flat/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[c, h] T2 → ∀J. T1 = ⓪{J} →
+fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[c, h] T2 → ∀J. T1 = ⓪{J} →
                         ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                          | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
-                         | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                         | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓓV1 & J = LRef 0 & c = cV
-                         | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                         | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
-                         | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+                         | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 &
                                         L = K.ⓑ{I}V & J = LRef (⫯i).
 #c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
 [ #I #G #L #J #H destruct /3 width=1 by or5_intro0, conj/
@@ -94,18 +94,18 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[c, h] T2 → ∀
 ]
 qed-.
 
-lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â\9e¡[c, h] T2 →
+lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â¬\88[c, h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                       | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
-                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓓV1 & J = LRef 0 & c = cV
-                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
-                      | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+                      | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[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: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡[c, h] T2 →
+lemma cpg_inv_sort1: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88[c, h] T2 →
                      (T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙).
 #c #h #G #L #T2 #s #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
@@ -115,11 +115,11 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 ]
 qed-.
 
-lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â\9e¡[c, h] T2 →
+lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â¬\88[c, h] T2 →
                      ∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
-                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓓV1 & c = cV
-                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+                      | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
 #c #h #G #L #T2 #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
@@ -129,9 +129,9 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
 ]
 qed-.
 
-lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â\9e¡[c, h] T2 →
+lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â¬\88[c, h] T2 →
                      (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
-                     â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+                     â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
 #c #h #G #L #T2 #i #H
 elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 [ #s #H destruct
@@ -140,7 +140,7 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
 ]
 qed-.
 
-lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â\9e¡[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
+lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â¬\88[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
 #c #h #G #L #T2 #l #H
 elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
 [ #s #H destruct
@@ -149,12 +149,12 @@ elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
 ]
 qed-.
 
-fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
                         ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
-                        â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+                        â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
                                        U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT
                         ) ∨
-                        â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+                        â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
                                 p = true & J = Abbr & c = (↓cT)+𝟙𝟘.
 #c #h #G #L #U #U2 * -c -G -L -U -U2
 [ #I #G #L #q #J #W #U1 #H destruct
@@ -172,26 +172,26 @@ fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ➡[c, h] U2 →
 ]
 qed-.
 
-lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] U2 → (
-                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[c, h] U2 → (
+                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                     U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT
                      ) ∨
-                     â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+                     â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[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: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â\9e¡[c, h] U2 → (
-                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abbr1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â¬\88[c, h] U2 → (
+                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                     U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT
                      ) ∨
-                     â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+                     â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[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 *
 /3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
 qed-.
 
-lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â\9e¡[c, h] U2 →
-                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â¬\88[c, h] U2 →
+                     â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â¬\88[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 * 
 [ /3 width=8 by ex4_4_intro/
@@ -199,15 +199,15 @@ lemma cpg_inv_abst1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[c, h]
 ]
 qed-.
 
-fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
                         ∀J,V1,U1. U = ⓕ{J}V1.U1 →
-                        â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+                        â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
                                           U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT
-                         | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
-                         | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
-                         | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                         | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
+                         | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
+                         | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                                         J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
-                         | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                         | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[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
@@ -225,23 +225,23 @@ fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ➡[c, h] U2 →
 ]
 qed-.
 
-lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â\9e¡[c, h] U2 →
-                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â¬\88[c, h] U2 →
+                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
                                        U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT
-                      | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
-                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
-                      | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                      | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
+                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
+                      | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                                      I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
-                      | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                      | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[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: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â\9e¡[c, h] U2 →
-                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â¬\88[c, h] U2 →
+                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
                                        U2 = ⓐV2.T2 & c = (↓cV)+cT
-                      | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                      | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
                                                      U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
-                      | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+                      | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[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/
@@ -251,11 +251,11 @@ lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡[c, h] U2 
 ]
 qed-.
 
-lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â\9e¡[c, h] U2 →
-                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â¬\88[c, h] U2 →
+                     â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
                                        U2 = ⓝV2.T2 & c = (↓cV)+cT
-                      | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & c = (↓cT)+𝟙𝟘
-                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & c = (↓cV)+𝟘𝟙.
+                      | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & c = (↓cT)+𝟙𝟘
+                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[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/
@@ -266,8 +266,8 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â\9e¡[c, h] T → ∀p.
-                           â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] ⓑ{p,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â¬\88[c, h] T → ∀p.
+                           â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[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 *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/