]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma
made executable again
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpm_cpx.ma
index 5251ac507408ec19aa9560c5dbe0ab3d0e5eb1cd..ea66025d5d9b48779ddd40685cd7a2dbb92e4237 100644 (file)
@@ -21,7 +21,7 @@ include "basic_2/rt_transition/cpm.ma".
 
 (* Basic_2A1: includes: cpr_cpx *)
 lemma cpm_fwd_cpx (h) (n) (G) (L):
-      â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬈ T2.
+      â\88\80T1,T2. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡[h,n] T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T1 ⬈ T2.
 #h #n #G #L #T1 #T2 * #c #_ #HT12
 /2 width=4 by cpg_cpx/
 qed-.