#R #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
/4 width=9 by sex_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/
qed-.
#R #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
/4 width=9 by sex_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/
qed-.