X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_tl.ma;h=3ef75c04cc87f76c0e20d591bf4c9c05eeaf641b;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=588f0d2242cdcbd0e6e24d7bc2fa4e295935f1e5;hpb=ad3d1cac216cf3882e4adf691b27c00838c6b9b1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
index 588f0d224..3ef75c04c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
@@ -28,14 +28,14 @@ interpretation "tail (rtmap)" 'DropPred f = (tl f).
 lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f.
 // qed.
 
-lemma tl_push_rew: ∀f. f = ⫱↑f.
+lemma tl_push_rew: ∀f. f = ⫱⫯f.
 #f <tl_rew <iota_push //
 qed.
 
-lemma tl_next_rew: ∀f. f = ⫱⫯f.
+lemma tl_next_rew: ∀f. f = ⫱↑f.
 #f <tl_rew <iota_next //
 qed.
 
-lemma tl_eq_repl: eq_repl … (λf1,f2. ⫱f1 ≗ ⫱f2).
+lemma tl_eq_repl: eq_repl … (λf1,f2. ⫱f1 ≡ ⫱f2).
 #f1 #f2 * -f1 -f2 //
 qed.