(* Properties with basic relocation *****************************************)
lemma lifts_lref_lt (m,n,i): i < m → ⇧[m,n] #i ≘ #i.
(* Properties with basic relocation *****************************************)
lemma lifts_lref_lt (m,n,i): i < m → ⇧[m,n] #i ≘ #i.