∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
/2 width=4 by vpushs_inv_unit_aux/ qed-.
(* Basic forward lemmas *****************************************************)
lemma vpushs_fwd_bind (M) (gv) (lv): is_model M →
∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
/2 width=4 by vpushs_inv_unit_aux/ qed-.
(* Basic forward lemmas *****************************************************)
lemma vpushs_fwd_bind (M) (gv) (lv): is_model M →