/5 width=3 by sex_refl, sex_next, sex_push, ext2_refl, ext2_pair, ex2_intro/
qed.
(* Advanced inversion lemmas ************************************************)
lemma rex_inv_bind_void (R):
/5 width=3 by sex_refl, sex_next, sex_push, ext2_refl, ext2_pair, ex2_intro/
qed.
(* Advanced inversion lemmas ************************************************)
lemma rex_inv_bind_void (R):