include "delayed_updating/syntax/label.ma".
include "ground/relocation/tr_pn.ma".
include "ground/lib/stream_tls.ma".
include "delayed_updating/syntax/label.ma".
include "ground/relocation/tr_pn.ma".
include "ground/lib/stream_tls.ma".
(* Basic constructions ******************************************************)
lemma prelift_rmap_d (f) (k:pnat):
(* Basic constructions ******************************************************)
lemma prelift_rmap_d (f) (k:pnat):