partial commit of the "dynamic" component

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
index 203cf3ebdfb3702ce36ba46e82e2ef2e04ea8086..88d19aea16c242799c53d0794f4a3424f80a1ee1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
@@ -37,7 +37,7 @@ qed.
 (* Inversion lemmas on "big tree" parallel reduction for closures ***********)
 
 lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ →
-                   h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ ∨ (L1 ➡ L2 ∧ T1 = T2).
+                   h â\8a¢ â¦\83L1, T1â¦\84 â\89»[g] â¦\83L2, T2â¦\84 â\88¨ (L1 â\8a¢ â\9e¡ L2 â\88§ T1 = T2).
 #h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/
 [ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/
 | #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/