milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / lpqs_lpqs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
index 566dd5347c19f3524b53630330c3bcc8562e6ae3..13f221e8657ec838625dcb80fddb6d8560beb2f8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma
@@ -24,7 +24,7 @@ fact cpqs_conf_lpqs_atom_atom:
 
 fact cpqs_conf_lpqs_atom_delta:
    ∀L0,i. (
-      ∀L,T.♯{L, T} < ♯{L0, #i} →
+      ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -39,7 +39,7 @@ elim (lpqs_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
 lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+lapply (fsupp_lref … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1)) #T #HVT
 lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
@@ -47,7 +47,7 @@ qed-.
 
 fact cpqs_conf_lpqs_delta_delta:
    ∀L0,i. (
-      ∀L,T.♯{L, T} < ♯{L0, #i} →
+      ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -67,7 +67,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
 elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
 lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+lapply (fsupp_lref … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1)) #T #HVT
 lapply (cpqs_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
@@ -76,7 +76,7 @@ qed-.
 
 fact cpqs_conf_lpqs_bind_bind:
    ∀a,I,L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} →
+      ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -93,7 +93,7 @@ qed-.
 
 fact cpqs_conf_lpqs_bind_zeta:
    ∀L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+      ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -110,7 +110,7 @@ qed-.
 
 fact cpqs_conf_lpqs_zeta_zeta:
    ∀L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+      ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -129,7 +129,7 @@ qed-.
 
 fact cpqs_conf_lpqs_flat_flat:
    ∀I,L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} →
+      ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -146,7 +146,7 @@ qed-.
 
 fact cpqs_conf_lpqs_flat_tau:
    ∀L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+      ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -161,7 +161,7 @@ qed-.
 
 fact cpqs_conf_lpqs_tau_tau:
    ∀L0,V0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+      ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L,T⦄ →
       ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
       ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
       ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
@@ -175,8 +175,8 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/
 qed-.
 
 theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs.
-#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
-[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*]
+[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpqs_inv_atom1 … H1) -H1
   elim (cpqs_inv_atom1 … H2) -H2
   [ #H2 #H1 destruct
@@ -189,7 +189,7 @@ theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs.
     * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
     /3 width=17 by cpqs_conf_lpqs_delta_delta/
   ]
-| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpqs_inv_bind1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1
   | #T1 #HT01 #HXT1 #H11 #H12
@@ -203,7 +203,7 @@ theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs.
   | /3 width=11 by cpqs_conf_lpqs_bind_zeta/
   | /3 width=12 by cpqs_conf_lpqs_zeta_zeta/
   ]
-| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpqs_inv_flat1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1
   | #HX1 #H1