[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, eq_id_inv_isid/
| /5 width=9 by s_rs_transitive_lex_inv_isid, sex_tc_dx, sex_co, ext2_tc, ex2_intro/
]
[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, eq_id_inv_isid/
| /5 width=9 by s_rs_transitive_lex_inv_isid, sex_tc_dx, sex_co, ext2_tc, ex2_intro/
]