qed.
(* Relocation properties ****************************************************)
(* Basic_1: was: nf2_lift *)
lemma cnf_lift: ∀L0,L,T,T0,d,e.
qed.
(* Relocation properties ****************************************************)
(* Basic_1: was: nf2_lift *)
lemma cnf_lift: ∀L0,L,T,T0,d,e.