- the relation for pointwise extensions now takes a binder as argument

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / llpx_sn_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
index bc8528408f5466dd7e016f36dbddf78e8e73dbc1..d0b9b2049620d4e7f873288c99c20efc0e5e6b3f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma
@@ -19,10 +19,10 @@ include "basic_2/relocation/llpx_sn.ma".
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
 (* alternative definition of llpx_sn *)
-inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
+inductive llpx_sn_alt (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝
 | llpx_sn_alt_intro: ∀L1,L2,T,d.
                      (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
-                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
+                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2
                      ) →
                      (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                         ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt R 0 V1 K1 K2
@@ -34,7 +34,7 @@ inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv len
 lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
                              (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                                 ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                                ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
+                                ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2
                              ) → llpx_sn_alt R d T L1 L2.
 #R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
@@ -45,7 +45,7 @@ lemma llpx_sn_alt_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
                            (∀L1,L2,T,d. |L1| = |L2| → (
                               ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                               ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                              ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 & S 0 V1 K1 K2
+                              ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 & S 0 V1 K1 K2
                            ) → S d T L1 L2) →
                            ∀L1,L2,T,d. llpx_sn_alt R d T L1 L2 → S d T L1 L2.
 #R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
@@ -58,7 +58,7 @@ lemma llpx_sn_alt_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 →
                            |L1| = |L2| ∧
                            ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                           ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
+                           ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2.
 #R #L1 #L2 #T #d #H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d
 #L1 #L2 #T #d #HL12 #IH @conj // -HL12
 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
@@ -103,7 +103,7 @@ lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 →
                              | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
                                                 ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
                                                 llpx_sn_alt R (yinj 0) V1 K1 K2 &
-                                                R K1 V1 V2 & d ≤ yinj i.
+                                                R I K1 V1 V2 & d ≤ yinj i.
 #R #L1 #L2 #d #i #H elim (llpx_sn_alt_inv_alt … H) -H
 #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
 elim (ylt_split i d) /3 width=1 by or3_intro1/
@@ -141,7 +141,7 @@ qed.
 
 lemma llpx_sn_alt_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
                         ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
-                        llpx_sn_alt R 0 V1 K1 K2 → R K1 V1 V2 →
+                        llpx_sn_alt R 0 V1 K1 K2 → R I K1 V1 V2 →
                         llpx_sn_alt R d (#i) L1 L2.
 #R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_intro_alt
 [ lapply (llpx_sn_alt_fwd_length … HK12) -HK12 #HK12
@@ -215,7 +215,7 @@ qed-.
 lemma llpx_sn_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                            ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2
+                            ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2
                          ) → llpx_sn R d T L1 L2.
 #R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_inv_lpx_sn
 @llpx_sn_alt_intro_alt // -HL12
@@ -227,7 +227,7 @@ lemma llpx_sn_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
                        (∀L1,L2,T,d. |L1| = |L2| → (
                           ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                           ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                          ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
+                          ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
                        ) → S d T L1 L2) →
                        ∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
 #R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
@@ -241,7 +241,7 @@ lemma llpx_sn_inv_alt: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
                        |L1| = |L2| ∧
                        ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
-                       ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
+                       ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
 #R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt … H) -H
 #H elim (llpx_sn_alt_inv_alt … H) -H
 #HL12 #IH @conj //