]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpb.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / lpr_fpb.ma
index 866a03b98a5c58c2ac2282b745dd7c800395bed9..e04ba82697f4c57118c85dfc435abb8a64027490 100644 (file)
@@ -21,5 +21,5 @@ include "basic_2/rt_transition/lpr_lpx.ma".
 
 (* Basic_2A1: uses: lpr_fpbq *)
 lemma lpr_fwd_fpb (h) (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â\9e¡[h,0] L2 â\86\92 â\9dªG,L1,Tâ\9d« â\89½ â\9dªG,L2,Tâ\9d«.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â\9e¡[h,0] L2 â\86\92 â\9d¨G,L1,Tâ\9d© â\89½ â\9d¨G,L2,Tâ\9d©.
 /3 width=2 by lpx_fpb, lpr_fwd_lpx/ qed-.