]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / lpr_lpx.ma
index ac7a93d628ea55ba6f92a5c31bd86fa8c7172dc0..d8b2c13908dd3c5928041a810f980d4ab30400d2 100644 (file)
@@ -22,5 +22,5 @@ include "basic_2/rt_transition/lpr.ma".
 
 (* Basic_2A1: was: lpr_lpx *)
 lemma lpr_fwd_lpx (h) (G):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â\9e¡[h,0] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈ L2.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â\9e¡[h,0] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈ L2.
 /3 width=3 by cpm_fwd_cpx, lex_co/ qed-.