milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_tl.ma

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 779cc4f6f82cf26259db74996bc2165f16592487..3ef75c04cc87f76c0e20d591bf4c9c05eeaf641b 100644 (file)
--- 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: â\88\80f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = â\86\93f.
+lemma tl_rew: â\88\80f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f.
 // qed.
 
-lemma tl_push_rew: â\88\80f. f = â\86\93â\86\91f.
+lemma tl_push_rew: â\88\80f. f = ⫱⫯f.
 #f <tl_rew <iota_push //
 qed.
 
-lemma tl_next_rew: â\88\80f. f = â\86\93⫯f.
+lemma tl_next_rew: â\88\80f. f = ⫱â\86\91f.
 #f <tl_rew <iota_next //
 qed.
 
-lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. â\86\93f1 â\89\97 â\86\93f2).
+lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. ⫱f1 â\89¡ ⫱f2).
 #f1 #f2 * -f1 -f2 //
 qed.