X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap.ma;h=8a2b7848b8d746fbb4d92556ad468beefe7679f2;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=f4120e31509a9168ba120676316f1ff48ea91d7a;hpb=b9526dac808d40bf89dc378cf9c5ea0c121526a4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma
index f4120e315..8a2b7848b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma
@@ -16,6 +16,6 @@ include "ground_2/relocation/nstream.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-lemma pn_split: ∀f. (∃g. ↑g = f) ∨ (∃g. ⫯g = f).
+lemma pn_split: ∀f. (∃g. ⫯g = f) ∨ (∃g. ↑g = f).
 @case_prop /3 width=2 by or_introl, or_intror, ex_intro/
 qed-.