X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_fcla.ma;h=26af72dfa27acc2c7dc302c5f4be4cd04fb77f8e;hb=ebc170efe71cf4ee842acfbe58bb6864e76ba98c;hp=14542cf48337d20e02a4c751af00cb145ac120e1;hpb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
index 14542cf48..26af72dfa 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
@@ -58,6 +58,22 @@ lemma fcla_inv_xp: ∀g,m. 𝐂⦃g⦄ ≡ m → 0 = m → 𝐈⦃g⦄.
 #g #m #_ #_ #H destruct
 qed-.
 
+lemma fcla_inv_isid: ∀f,n. 𝐂⦃f⦄ ≡ n → 𝐈⦃f⦄ → 0 = n.
+#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
+#f #n #_ #_ #H elim (isid_inv_next … H) -H //  
+qed-.
+
+(* Main forward lemmas ******************************************************)
+
+theorem fcla_mono: ∀f,n1. 𝐂⦃f⦄ ≡ n1 → ∀n2. 𝐂⦃f⦄ ≡ n2 → n1 = n2.
+#f #n #H elim H -f -n
+[ /2 width=3 by fcla_inv_isid/
+| /3 width=3 by fcla_inv_px/
+| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx … H) -H [2,3 : // ]
+  #g #Hf #H destruct /3 width=1 by eq_f/
+]
+qed-.
+
 (* Basic properties *********************************************************)
 
 lemma fcla_eq_repl_back: ∀n. eq_repl_back … (λf. 𝐂⦃f⦄ ≡ n).