L1 ≛[V] L2 ∧ L1.ⓧ ≛[T] L2.ⓧ.
/2 width=3 by rex_inv_bind_void/ qed-.
(* Advanced forward lemmas **************************************************)
lemma reqx_fwd_bind_dx_void: ∀p,I,L1,L2,V,T.
L1 ≛[V] L2 ∧ L1.ⓧ ≛[T] L2.ⓧ.
/2 width=3 by rex_inv_bind_void/ qed-.
(* Advanced forward lemmas **************************************************)
lemma reqx_fwd_bind_dx_void: ∀p,I,L1,L2,V,T.