include "ground/lib/stream_hdtl.ma".
include "ground/relocation/gr_map.ma".
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
(*** tl *)
definition gr_tl (f): gr_map ≝ ⫰f.
"tail (generic relocation maps)"
'DropPred f = (gr_tl f).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** tl_push_rew *)
lemma gr_tl_push (f): f = ⫱⫯f.
lemma gr_tl_next (f): f = ⫱↑f.
// qed.
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
(*** pn_split gr_map_split *)
lemma gr_map_split_tl (f): ∨∨ ⫯⫱f = f | ↑⫱f = f.