lambdadelta

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index c1b30c334b30ccffc532ad8d66c438b6bca9fc6a..b593d637de03bb4cb7676417d5716a902a0920a8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/btpredstarproper_6.ma".
 include "basic_2/dynamic/ysc.ma".
 include "basic_2/dynamic/yprs.ma".
 
@@ -65,8 +66,9 @@ lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
 /3 width=4 by ygt_strap2/
 qed-.
 
-lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
+lemma fsupp_ygt: ∀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_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
                 h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.