Y1 = L1.โค{I} & Y2 = L2.โค{I}.
#Y1 #Y2 #H elim (rex_inv_zero โฆ H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
Y1 = L1.โค{I} & Y2 = L2.โค{I}.
#Y1 #Y2 #H elim (rex_inv_zero โฆ H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/