]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
update in ground, static_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_compose_etc.ma
index 663dfc9b68684cd431e14aaffa4630496dae2a0f..4c8586c31c9deb75d53d58df8f2d66b7f62d5be8 100644 (file)
@@ -89,7 +89,7 @@ lemma after_inv_const: ∀f2,f1,f,p1,p.
 ]
 qed-.
 
-lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
+lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\90 f.
 /2 width=4 by gr_after_mono/ qed-.
 
 (* Forward lemmas on after (specific) *****************************************)