]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma
milestone update in ground_2 and basic_2A
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap.ma
index f4120e31509a9168ba120676316f1ff48ea91d7a..8a2b7848b8d746fbb4d92556ad468beefe7679f2 100644 (file)
@@ -16,6 +16,6 @@ include "ground_2/relocation/nstream.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-lemma pn_split: â\88\80f. (â\88\83g. â\86\91g = f) â\88¨ (â\88\83g. â«¯g = f).
+lemma pn_split: â\88\80f. (â\88\83g. â«¯g = f) â\88¨ (â\88\83g. â\86\91g = f).
 @case_prop /3 width=2 by or_introl, or_intror, ex_intro/
 qed-.