/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Basic inversion properties ***********************************************)
lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):
/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
(* Basic inversion properties ***********************************************)
lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):