X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_coafter.ma;h=4864c9bae037f151c403f9d309d898701c6b52ca;hb=57296e7036707343c4d8a8e990a48e5f1518eee4;hp=c6e4b3a960368be5384b66f1f5d6695ac42d7039;hpb=5ea718c8b65a9ca62e8b602800667259b8b2d090;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
index c6e4b3a96..4864c9bae 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -151,6 +151,14 @@ lemma coafter_inv_xxn: ∀g1,g2,g. g1 ~⊚ g2 ≡ g → ∀f. ⫯f = g →
 ]
 qed-.
 
+lemma coafter_inv_xnn: ∀g1,g2,g. g1 ~⊚ g2 ≡ g →
+                       ∀f2,f. ⫯f2 = g2 → ⫯f = g →
+                       ∃∃f1. f1 ~⊚ f2 ≡ f & ↑f1 = g1.
+#g1 #g2 #g #Hg #f2 #f #H2 destruct #H
+elim (coafter_inv_xxn … Hg … H) -g
+#z1 #z2 #Hf #H1 #H2 destruct /2 width=3 by ex2_intro/
+qed-.
+
 lemma coafter_inv_xxp: ∀g1,g2,g. g1 ~⊚ g2 ≡ g → ∀f. ↑f = g →
                        (∃∃f1,f2. f1 ~⊚ f2 ≡ f & ↑f1 = g1 & ↑f2 = g2) ∨
                        ∃∃f1. f1 ~⊚ g2 ≡ f & ⫯f1 = g1.