/3 width=7 by frees_fwd_isfin, frees_flat, sex_join, ex2_intro/
qed.
theorem rex_bind_void (R) (p) (I):
∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2.
#R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
/3 width=7 by frees_fwd_isfin, frees_flat, sex_join, ex2_intro/
qed.
theorem rex_bind_void (R) (p) (I):
∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2.
#R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2