- induction on supclosure replaces induction on weight for closures everywhere

- bug fix in csn_alt

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma
index 5dd59df28c39e77a1148122aa7d23dad1a745e1b..9a315478497d0a6d244a78974271292776d7021c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma
@@ -51,7 +51,7 @@ lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢
 elim (term_eq_dec T1 T2) #HT12
 [ -IHT1 -HLT12 destruct /3 width=1/
 | -HT1 -HT2 /3 width=4/
-qed.
+qed-.
 
 (* Basic_1: was: sn3_cast *)
 lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. T.
@@ -60,10 +60,10 @@ lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW.
 elim (cpr_inv_cast1 … H1) -H1
 [ * #W0 #T0 #HLW0 #HLT0 #H destruct
   elim (eq_false_inv_tpair_sn … H2) -H2
-  [ /3 width=3/
+  [ /3 width=3 by csn_cpr_trans/
   | -HLW0 * #H destruct /3 width=1/
   ]
-| /3 width=3/
+| /3 width=3 by csn_cpr_trans/
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
index c880b2dd2f632b56ca2db5f157b13c4cc4ab341e..eb10f09818e077415d658eb1607dd393650b72e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
@@ -83,7 +83,8 @@ qed.
 
 (* Basic_1: was: sn3_pr3_trans *)
 lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊* T2.
-/4 width=3/ qed.
+#L #T1 #HT1 #T2 #H @(cprs_ind … H) -T2 // /2 width=3 by csn_cpr_trans/
+qed-.
 
 (* Main eliminators *********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
index 1919c111a793bc82670d518aaeac5c18a0b1a285..14da3109709f4c6afd32c2a8b5460e66fbe33f3a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
@@ -63,7 +63,7 @@ lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T →
 elim (cpr_fwd_abst1 … H1 I V) -H1
 #W0 #T0 #HLW0 #HLT0 #H destruct
 elim (eq_false_inv_tpair_sn … H2) -H2
-[ /3 width=5/
+[ /3 width=5 by csn_cpr_trans/
 | -HLW0 * #H destruct /3 width=1/
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma
index da3337eee03af887f2e1f32200a498326bd95628..b406fa3f19b2a051249f29d2b5a1558278580502 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma
@@ -34,7 +34,7 @@ elim (cpr_inv_abbr1 … H1) -H1 *
 [ #V1 #T1 #HLV1 #HLT1 #H destruct
   elim (eq_false_inv_tpair_sn … H2) -H2
   [ #HV1 @IHV // /2 width=1/ -HV1
-    @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
+    @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpr_trans/
   | -IHV -HLV1 * #H destruct /3 width=1/
   ]
 | -IHV -IHT -H2 #T0 #HLT0 #HT0
@@ -54,15 +54,15 @@ elim (cpr_inv_appl1 … H) -H *
   elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
   elim (eq_false_inv_beta … H2) -H2
   [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
-    @csn_abbr /2 width=3/ -HV
-    @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3/
+    @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
+    @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/
   | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
     @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/
   ]
 | -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
   lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01
-  @csn_abbr /2 width=3/ -HV
-  @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+  @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
+  @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/
 | -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
 ]
 qed-.
@@ -103,7 +103,7 @@ elim (cpr_inv_appl1 … HL) -HL *
 | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
 | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
   lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
-  @csn_abbr /2 width=3/ -HV
+  @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
   @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1
   @(csn_cprs_trans … HVT) -HVT /3 width=1/
 ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index 2a98026260c12c63b5953448775dc02db4ebc718..1f79433bd98a2c9608cd6c8c6580f68cd6b24c58 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -28,12 +28,6 @@ lemma fw_shift: ∀a,K,I,V,T. ♯{K. ⓑ{I} V, T} < ♯{K, ⓑ{a,I} V. T}.
 normalize //
 qed.
 
-lemma tw_shift: ∀L,T. ♯{L, T} ≤ ♯{L @@ T}.
-#L elim L //
-#K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
-qed.
-
 lemma fw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}.
 normalize in ⊢ (?→?→?→?→?%%); //
 qed.
@@ -42,26 +36,12 @@ lemma fw_tpair_dx: ∀I,L,V,T. ♯{L, T} < ♯{L, ②{I}V.T}.
 normalize in ⊢ (?→?→?→?→?%%); //
 qed.
 
-lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
-qed.
-
-lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
-                            ♯{L.ⓑ{I}V1, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/
-qed.
-
-lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
-                            ♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *)
-qed.
-
 lemma fw_lpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L.ⓑ{I}V, T}.
 normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
 qed.
 
 (* Basic_1: removed theorems 7:
-            flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
-            flt_wf_ind
+            flt_thead_sx flt_thead_dx flt_trans
+            flt_arith0 flt_arith1 flt_arith2 flt_wf_ind
 *)
 (* Basic_1: removed local theorems 1: q_ind *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index f9a63718a5d6ed6f04e18d26d0fb2d04b9855de3..fc3b65c60d94e962ea40dac00163522fad891ec2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
-include "basic_2/relocation/fsup.ma".
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/reduction/lpr_ldrop.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
@@ -26,7 +26,7 @@ fact cpr_conf_lpr_atom_atom:
 
 fact cpr_conf_lpr_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
@@ -41,7 +41,7 @@ elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_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 (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
@@ -50,7 +50,7 @@ qed-.
 (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *)
 fact cpr_conf_lpr_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
@@ -70,7 +70,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_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 (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
@@ -79,7 +79,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -96,7 +96,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -113,7 +113,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -132,7 +132,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -149,7 +149,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -164,7 +164,7 @@ qed-.
 
 fact cpr_conf_lpr_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
@@ -179,7 +179,7 @@ qed-.
 
 fact cpr_conf_lpr_flat_beta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 →
       ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0
@@ -202,7 +202,7 @@ qed-.
 *)
 fact cpr_conf_lpr_flat_theta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 →
       ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0
@@ -231,7 +231,7 @@ qed-.
 
 fact cpr_conf_lpr_beta_beta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 →
       ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0
@@ -251,7 +251,7 @@ qed-.
 (* Basic_1: was: pr0_upsilon_upsilon *)
 fact cpr_conf_lpr_theta_theta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 →
       ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0
@@ -274,8 +274,8 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/
 qed-.
 
 theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr.
-#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 (cpr_inv_atom1 … H1) -H1
   elim (cpr_inv_atom1 … H2) -H2
   [ #H2 #H1 destruct
@@ -288,7 +288,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr.
     * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
     /3 width=17 by cpr_conf_lpr_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 (cpr_inv_bind1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1
   | #T1 #HT01 #HXT1 #H11 #H12
@@ -302,7 +302,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr.
   | /3 width=11 by cpr_conf_lpr_bind_zeta/
   | /3 width=12 by cpr_conf_lpr_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 (cpr_inv_flat1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1
   | #HX1 #H1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma
index 060f216487dfea03449f3f9b034ea99d16ef878c..9ce690f683a359223d09433be107fee81d4a0df3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/substitution/lpss_ldrop.ma".
 include "basic_2/reduction/lpr_ldrop.ma".
 
@@ -26,7 +27,7 @@ fact cpr_cpss_conf_lpr_lpss_atom_atom:
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -41,7 +42,7 @@ elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpss_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 (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
@@ -49,7 +50,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_delta_atom:
    ∀L0,i. (
-      â\88\80L,T.â\99¯{L, T} < â\99¯{L0, #i} →
+      â\88\80L,T.â¦\83L0, #iâ¦\84 â\8a\83+ â¦\83L, Tâ¦\84 →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 →
       ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0
@@ -64,7 +65,7 @@ elim (lpss_inv_pair1 … H2) -H2 #K2 #V2 #HK02 #HV02 #H destruct
 elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
 elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
 lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
-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 (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 /3 width=9/
@@ -72,7 +73,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -92,7 +93,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
 elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpss_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 (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
@@ -101,7 +102,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -118,7 +119,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -135,7 +136,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -152,7 +153,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_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
@@ -167,7 +168,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_flat_beta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 →
       ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0
@@ -186,7 +187,7 @@ qed-.
 
 fact cpr_cpss_conf_lpr_lpss_flat_theta:
    ∀a,L0,V0,W0,T0. (
-      ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} →
+      ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ →
       ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 →
       ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 →
       ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0
@@ -208,8 +209,8 @@ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T
 qed-.
 
 lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss.
-#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 (cpr_inv_atom1 … H1) -H1
   elim (cpss_inv_atom1 … H2) -H2
   [ #H2 #H1 destruct
@@ -222,7 +223,7 @@ lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss.
     * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
     /3 width=17 by cpr_cpss_conf_lpr_lpss_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 (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2
   elim (cpr_inv_bind1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1
@@ -231,7 +232,7 @@ lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss.
   [ /3 width=10 by cpr_cpss_conf_lpr_lpss_bind_bind/
   | /3 width=11 by cpr_cpss_conf_lpr_lpss_bind_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 (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2
   elim (cpr_inv_flat1 … H1) -H1 *
   [ #V1 #T1 #HV01 #HT01 #H1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
index cffa08c68bc0b4c6909508d3b62b9ae4973c966e..16fbeb12889085acebf415913168798d752398c6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/cl_weight.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* SUPCLOSURE ***************************************************************)
@@ -46,7 +47,7 @@ qed.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma fsup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+lemma fsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
 lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 85d36c39f610b394293b6d9e8dd2f6b0947b7f84..7d3b3b0ce73e2a9337a766342b4cc148dda21895 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/cl_weight.ma".
+include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_weight.ma".
 include "basic_2/relocation/lift.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
@@ -246,6 +247,14 @@ qed.
 
 (* Basic forvard lemmas *****************************************************)
 
+lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
+[ /2 width=3/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
+  >(lift_fwd_tw … HV21) -HV21 /2 width=1/
+]
+qed-.
+
 (* Basic_1: was: drop_S *)
 lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
                         ⇩[O, e + 1] L1 ≡ K2.
@@ -263,21 +272,6 @@ lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/
 qed-.
 
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
-[ /2 width=3/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
-  >(lift_fwd_tw … HV21) -HV21 /2 width=1/
-]
-qed-.
-
-lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
-                          ∀T. ♯{K, V} < ♯{L, T}.
-#I #L #K #V #d #e #H #T
-lapply (ldrop_fwd_lw … H) -H #H
-@(le_to_lt_to_lt … H) -H /3 width=1/
-qed-.
-
 lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
                                ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
 #L1 elim L1 -L1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
index 7629115761cdb8f186a349817d90775b68f92468..6cae606c7208e2c7ebf47322a2fdfa6bde240227 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lenv_append.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* DROPPING *****************************************************************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
index f6bae4fa2e452eb5a0048f24cc1da322a563bf48..a10cc99f596df793048b252ed9b29399438298ae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/cl_shift.ma".
 include "basic_2/relocation/ldrop_append.ma".
 include "basic_2/substitution/lsubr.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
index 149a6bd82b1388ebe8835b088c2dad0b132b44bd..fb75c7338fcb9afd7b6117160b46233bffc7ae84 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma
@@ -21,24 +21,6 @@ definition fsupp: bi_relation lenv term ≝ bi_TC … fsup.
 interpretation "plus-iterated structural successor (closure)"
    'SupTermPlus L1 T1 L2 T2 = (fsupp L1 T1 L2 T2).
 
-(* Basic eliminators ********************************************************)
-
-lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
-                 (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) →
-                 (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) →
-                 ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2.
-#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
-@(bi_TC_ind … IH1 IH2 ? ? H)
-qed-.
-
-lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
-                    (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) →
-                    (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) →
-                    ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1.
-#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
-@(bi_TC_ind_dx … IH1 IH2 ? ? H)
-qed-.
-
 (* Basic properties *********************************************************)
 
 lemma fsup_fsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
@@ -79,9 +61,36 @@ lemma fsupp_append_sn: ∀I,L,K,V,T. ⦃L.ⓑ{I}V@@K, T⦄ ⊃+ ⦃L, V⦄.
 normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
 qed.
 *)
+(* Basic eliminators ********************************************************)
+
+lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term.
+                 (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) →
+                 (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) →
+                 ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_TC_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+                    (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) →
+                    (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) →
+                    ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_TC_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
-lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
+lemma fsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
 #L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -L2 -T2
-/3 width=3 by fsup_fwd_cw, transitive_lt/
+/3 width=3 by fsup_fwd_fw, transitive_lt/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma fsupp_wf_ind: ∀R:relation2 lenv term. (
+                       ∀L1,T1. (∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2) →
+                       ∀L2,T2. L1 = L2 → T1 = T2 → R L2 T2
+                    ) → ∀L1,T1. R L1 T1.
+#R #HR @(f2_ind … fw) #n #IHn #L1 #T1 #H destruct /4 width=5 by fsupp_fwd_fw/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
index d915b89f10290853bff78338aeda8981393880a7..07a7b836df8a15a1dde186f96da1d68d44d9bfd4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
@@ -63,17 +63,12 @@ lemma fsups_fsupp_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ →
 lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ →
                          ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
 /2 width=4/ qed.
-(*
-lemma fsups_pippo: ∀L,T. ⦃L, T⦄ ⊃+ ⦃L, #0⦄.
-#L * *
-[ #i 
-*)
 
 (* Basic forward lemmas *****************************************************)
 
-lemma fsups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+lemma fsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 //
-/4 width=3 by fsup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
+/4 width=3 by fsup_fwd_fw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *)
 qed-.
 (*
 (* Advanced inversion lemmas on plus-iterated supclosure ********************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
index c9c17fa19d788f5b7db566e95d7386ab35af64be..71ab873af3d4bd97b2cfa7e35d689d5d8e6cbc87 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/substitution/lpss_ldrop.ma".
 
 (* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************)
@@ -20,8 +21,8 @@ include "basic_2/substitution/lpss_ldrop.ma".
 (* Main properties on context-sensitive parallel substitution for terms *****)
 
 theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss.
-#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
-[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L0 #T0 #IH #L1 * [|*]
+[ #I #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct
   elim (cpss_inv_atom1 … H1) -H1
   [ #H destruct
     elim (cpss_inv_atom1 … HT2) -HT2
@@ -29,19 +30,19 @@ theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss.
     | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
       elim (lpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
       elim (lpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
-      lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+      lapply (fsupp_lref … HLK1) /3 width=9/
     ]
   | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
     elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
     elim (lpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
     elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
-    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+    lapply (fsupp_lref … HLK1) /3 width=9/
   ]
-| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+| #a #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
   elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
   elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
-| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+| #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
   elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
   elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
 ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
index ad972cd4a249a0200c71b7f1e50bfa55d4e88a6b..12bb02b070bdf1837d96bdb61d14f71dbfeb0892 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma
@@ -24,7 +24,7 @@ fact cpss_conf_lpss_atom_atom:
 
 fact cpss_conf_lpss_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 (lpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpss_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 (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
@@ -47,7 +47,7 @@ qed-.
 
 fact cpss_conf_lpss_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 (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpss_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 (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
@@ -76,7 +76,7 @@ qed-.
 
 fact cpss_conf_lpss_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 cpss_conf_lpss_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
@@ -109,8 +109,8 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
 qed-.
 
 theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss.
-#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 (cpss_inv_atom1 … H1) -H1
   elim (cpss_inv_atom1 … H2) -H2
   [ #H2 #H1 destruct
@@ -123,11 +123,11 @@ theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss.
     * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
     /3 width=17 by cpss_conf_lpss_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 (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
   elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
   /3 width=10 by cpss_conf_lpss_bind_bind/
-| #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 (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
   elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
   /3 width=10 by cpss_conf_lpss_flat_flat/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
index fb94a49de339af9ef7ad61e09d10de3ad781e93d..7b8f17b4a5b12a3b843f0d50d693fbccab0667d5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/unfold/lpqs_ldrop.ma".
 
 (* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
@@ -20,8 +21,8 @@ include "basic_2/unfold/lpqs_ldrop.ma".
 (* Main properties on context-sensitive rest parallel computation for terms *)
 
 theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs.
-#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
-[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L0 #T0 #IH #L1 * [|*]
+[ #I #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct
   elim (cpqs_inv_atom1 … H1) -H1
   [ #H destruct
     elim (cpqs_inv_atom1 … HT2) -HT2
@@ -29,16 +30,16 @@ theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs.
     | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
       elim (lpqs_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
       elim (lpqs_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
-      lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+      lapply (fsupp_lref … HLK1) /3 width=9/
     ]
   | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
     elim (lpqs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
     elim (lpqs_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
     elim (cpqs_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
-    lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+    lapply (fsupp_lref … HLK1) /3 width=9/
   ]
-| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+| #a #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
   elim (cpqs_inv_bind1 … H1) -H1 *
   [ #V #T #HV1 #HT1 #H destruct
     elim (cpqs_inv_bind1 … H2) -H2 *
@@ -49,7 +50,7 @@ theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs.
     elim (lift_total X2 0 1) #Y2 #HXY2
     lapply (cpqs_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/
   ]
-| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+| #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
   elim (cpqs_inv_flat1 … H1) -H1 *
   [ #V #T #HV1 #HT1 #H destruct
     elim (cpqs_inv_flat1 … H2) -H2 *

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
index 4235f281ee1a65a48a1189db9625f3823c88e836..42af90e61346602df09d59bf62dd503c8ef3cf53 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lenv_append.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* CONTEXT-SENSITIVE UNFOLD FOR TERMS ***************************************)