- basic_2: induction for preservation results now uses supclosure

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / yprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index 2bf1ae018495ab4476371e9c52ef4119c96668f0..08461cda5d6d5e878afde43b1e3b8b78b35bded1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/computation/lprs.ma".
 include "basic_2/dynamic/ypr.ma".
 
@@ -52,9 +53,11 @@ lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄
                    h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
 /2 width=4/ qed-.
 
-lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} →
-               h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
+(* Note: this is a general property of bi_TC *)
+lemma fsupp_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ →
+                  h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+qed.
 
 lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
 #h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/