(* Note: probably this is an inversion lemma *)
(* Basic_2A1: was: cpxs_fwd_delta *)
lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
(* Note: probably this is an inversion lemma *)
(* Basic_2A1: was: cpxs_fwd_delta *)
lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →