1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/functions/droppred_1.ma".
16 include "ground_2/relocation/rtmap_eq.ma".
18 (* RELOCATION MAP ***********************************************************)
20 definition tl: rtmap → rtmap.
24 interpretation "tail (rtmap)" 'DropPred f = (tl f).
26 (* Basic properties *********************************************************)
28 lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f.
31 lemma tl_push_rew: ∀f. f = ⫱↑f.
32 #f <tl_rew <iota_push //
35 lemma tl_next_rew: ∀f. f = ⫱⫯f.
36 #f <tl_rew <iota_next //
39 lemma tl_eq_repl: eq_repl … (λf1,f2. ⫱f1 ≗ ⫱f2).