∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
/2 width=4 by li_inv_unit_aux/ qed-.
(* Advanced forward lemmas **************************************************)
lemma li_fwd_bind (M) (gv): is_model M →
∃∃lv,d. lv ϵ ⟦L⟧[gv] & ⫯[0←d]lv ≗ v.
/2 width=4 by li_inv_unit_aux/ qed-.
(* Advanced forward lemmas **************************************************)
lemma li_fwd_bind (M) (gv): is_model M →