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=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;hp=779cc4f6f82cf26259db74996bc2165f16592487;hpb=b9526dac808d40bf89dc378cf9c5ea0c121526a4;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 779cc4f6f..3ef75c04c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/notation/functions/droppred_1.ma".
 include "ground_2/relocation/rtmap_eq.ma".
 
 (* RELOCATION MAP ***********************************************************)
@@ -21,21 +21,21 @@ definition tl: rtmap → rtmap.
 @case_type0 #f @f
 defined.
 
-interpretation "tail (rtmap)" 'Drop f = (tl f).
+interpretation "tail (rtmap)" 'DropPred f = (tl f).
 
 (* Basic properties *********************************************************)
 
-lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ↓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.