/5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
]
qed.
(* Basic_2A1: was: cpxs_delta *)
lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
/5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
]
qed.
(* Basic_2A1: was: cpxs_delta *)
lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.