]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
update in ground, static_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sor_sor.ma
index ef667fd7ebfcf530096c8efdaedace0445af1bfd..c52154795c318fb25de1a7e79e2e2e9dcf3d4890 100644 (file)
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sor.ma".
 
 (*** sor_mono *)
 corec theorem pr_sor_mono:
-              â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89¡ y.
+              â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89\90 y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
 [ cases (pr_sor_inv_push_bi … H … H1 H2)