first definition of cpm:

[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..fd44b81fd8816cbf44f0e1b11cdc01e13cbb703e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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".
@@ -29,7 +28,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
 | 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
+             ⬆*[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
 | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2.
@@ -39,44 +38,44 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
              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
+             ⬆*[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_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 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 h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
 .
 
 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 &
-                                         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\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 â¬\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 +93,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 &
-                                      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\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 â¬\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,12 +114,12 @@ 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 &
-                                      L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
+                      | â\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/
 [ #s #H destruct
@@ -129,9 +128,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 +139,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,13 +148,13 @@ 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 &
-                                p = true & J = Abbr & c = (↓cT)+𝟙𝟘.
+                        â\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
 | #G #L #s #q #J #W #U1 #H destruct
@@ -172,26 +171,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 &
-                             p = true & I = Abbr & c = (↓cT)+𝟙𝟘.
+                     â\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 &
-                             p = true & c = (↓cT)+𝟙𝟘.
+                     â\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,16 +198,16 @@ 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 = (â\86\93cT)+𝟙𝟘
-                         | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & J = Cast & c = (â\86\93cV)+𝟘𝟙
-                         | â\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 &
-                                                        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 &
-                                                          J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
+                         | â\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 â¬\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
 | #G #L #s #J #W #U1 #H destruct
@@ -225,24 +224,24 @@ 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 = (â\86\93cT)+𝟙𝟘
-                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & I = Cast & c = (â\86\93cV)+𝟘𝟙
-                      | â\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 &
-                                                     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 &
-                                                       I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
+                      | â\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 â¬\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 &
-                                                     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 &
-                                                       U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
+                      | â\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 â¬\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/
 |2,3: #c #_ #H destruct
@@ -251,11 +250,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 = (â\86\93cT)+𝟙𝟘
-                      | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & c = (â\86\93cV)+𝟘𝟙.
+                      | â\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 +265,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/