Theorem Sum.elim_comp_inl_inr

Modification history