X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pn.ma;h=c38aad7123b995af280a7443ef6fc21b4c2d1399;hb=70e25b49cc5bc42e7eac421d0c74b00e4fb09b74;hp=2418afd112cb4f0cff5fac4a3ccaee22f5f8c66b;hpb=3e69f22d5d147107a3c79ff9301b006d0c8d644f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
index 2418afd11..c38aad712 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
@@ -47,3 +47,12 @@ lemma tr_inj_push (f): ⫯𝐭❨f❩ = 𝐭❨⫯f❩.
 lemma tr_inj_next (f): ↑𝐭❨f❩ = 𝐭❨↑f❩.
 * //
 qed.
+
+(* Basic eliminations *******************************************************)
+
+lemma tr_map_split (f:tr_map):
+      ∨∨ ∃g. ⫯g = f
+       | ∃g. ↑g = f.
+* *
+/3 width=2 by ex_intro, or_introl, or_intror/
+qed-.