update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_pn.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
index 2418afd112cb4f0cff5fac4a3ccaee22f5f8c66b..c38aad7123b995af280a7443ef6fc21b4c2d1399 100644 (file)
--- 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-.