X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flsubc.ma;h=bb4b27fe317d3d7d2152ece3d09e47db058df94a;hp=7b5315d4fb1b3653b0118a0b4c8747b3f3d2caf1;hb=222044da28742b24584549ba86b1805a87def070;hpb=38571b4c3881f2b59b7a2cdd016c83b161d3d755

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma
index 7b5315d4f..bb4b27fe3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma
@@ -20,7 +20,7 @@ include "basic_2/static/gcp_cr.ma".
 
 inductive lsubc (RP) (G): relation lenv ≝
 | lsubc_atom: lsubc RP G (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubc_bind: ∀I,L1,L2. lsubc RP G L1 L2 → lsubc RP G (L1.ⓘ{I}) (L2.ⓘ{I})
 | lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
               lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
 .
@@ -34,7 +34,7 @@ interpretation
 fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 = ⋆ → L2 = ⋆.
 #RP #G #L1 #L2 * -L1 -L2
 [ //
-| #I #L1 #L2 #V #_ #H destruct
+| #I #L1 #L2 #_ #H destruct
 | #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
 ]
 qed-.
@@ -43,30 +43,31 @@ qed-.
 lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆.
 /2 width=5 by lsubc_inv_atom1_aux/ qed-.
 
-fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                          (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+fact lsubc_inv_bind1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1. L1 = K1.ⓘ{I} →
+                          (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓘ{I}) ∨
                           ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
                                       G ⊢ K1 ⫃[RP] K2 &
-                                      L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+                                      L2 = K2. ⓛW & I = BPair Abbr (ⓝW.V).
 #RP #G #L1 #L2 * -L1 -L2
-[ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/
+[ #I #K1 #H destruct
+| #J #L1 #L2 #HL12 #I #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #H destruct
+  /3 width=10 by ex6_4_intro, or_intror/
 ]
 qed-.
 
 (* Basic_1: was: csubc_gen_head_r *)
-lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃[RP] L2 →
-                       (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+lemma lsubc_inv_bind1: ∀RP,I,G,K1,L2. G ⊢ K1.ⓘ{I} ⫃[RP] L2 →
+                       (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓘ{I}) ∨
                        ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
                                    G ⊢ K1 ⫃[RP] K2 &
-                                   L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
-/2 width=3 by lsubc_inv_pair1_aux/ qed-.
+                                   L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V).
+/2 width=3 by lsubc_inv_bind1_aux/ qed-.
 
 fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L2 = ⋆ → L1 = ⋆.
 #RP #G #L1 #L2 * -L1 -L2
 [ //
-| #I #L1 #L2 #V #_ #H destruct
+| #I #L1 #L2 #_ #H destruct
 | #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
 ]
 qed-.
@@ -75,31 +76,32 @@ qed-.
 lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⫃[RP] ⋆ → L1 = ⋆.
 /2 width=5 by lsubc_inv_atom2_aux/ qed-.
 
-fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
-                          (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓑ{I} W) ∨
-                          ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                    G ⊢ K1 ⫃[RP] K2 &
-                                    L1 = K1.ⓓⓝW.V & I = Abst.
+fact lsubc_inv_bind2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2. L2 = K2.ⓘ{I} →
+                          (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓘ{I}) ∨
+                          ∃∃K1,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                      G ⊢ K1 ⫃[RP] K2 &
+                                      L1 = K1.ⓓⓝW.V & I = BPair Abst W.
 #RP #G #L1 #L2 * -L1 -L2
-[ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/
+[ #I #K2 #H destruct
+| #J #L1 #L2 #HL12 #I #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #H destruct
+  /3 width=10 by ex6_4_intro, or_intror/
 ]
 qed-.
 
 (* Basic_1: was just: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
-                       (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓑ{I} W) ∨
-                       ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                 G ⊢ K1 ⫃[RP] K2 &
-                                 L1 = K1.ⓓⓝW.V & I = Abst.
-/2 width=3 by lsubc_inv_pair2_aux/ qed-.
+lemma lsubc_inv_bind2: ∀RP,I,G,L1,K2. G ⊢ L1 ⫃[RP] K2.ⓘ{I} →
+                       (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓘ{I}) ∨
+                       ∃∃K1,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                   G ⊢ K1 ⫃[RP] K2 &
+                                   L1 = K1.ⓓⓝW.V & I = BPair Abst W.
+/2 width=3 by lsubc_inv_bind2_aux/ qed-.
 
 (* Basic properties *********************************************************)
 
 (* Basic_1: was just: csubc_refl *)
 lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L.
-#RP #G #L elim L -L /2 width=1 by lsubc_pair/
+#RP #G #L elim L -L /2 width=1 by lsubc_bind/
 qed.
 
 (* Basic_1: removed theorems 3: