- basic_2: induction for preservation results now uses supclosure

[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 85419d1eaa3b9358a2e87815f9b5a998855a2853..3e1cccb4e50b445ed08d22f5de4e0c9c17eddf57 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/yprs.ma".
 inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝
 | ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ →
             ygt h g L1 T1 L2 T2
-| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T
+| ygt_step: â\88\80L,L2,T. ygt h g L1 T1 L T â\86\92 L â\8a¢ â\9e¡ L2 â\86\92 ygt h g L1 T1 L2 T
 .
 
 interpretation "'big tree' proper parallel computation (closure)"
@@ -31,7 +31,7 @@ interpretation "'big tree' proper parallel computation (closure)"
 lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ →
                     h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
 #h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2
-/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/
+/3 width=4 by yprs_strap1, ysc_ypr, ypr_lpr/
 qed-.
 
 (* Basic properties *********************************************************)
@@ -65,8 +65,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⦄.
@@ -94,6 +95,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → 
 ]
 qed.
 
-lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) →
+lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) →
                   h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄.
 /4 width=1/ qed.