proposition: Lemma opp_opp : forall a, opp (opp a) = a.
proof: Proof. ir. apply by_cases with (axioms a); ir. assert (opp a = opp' a). uf opp. ap (Y_if H). tv. rw H0. assert (axioms (opp' a)). ap opp'_axioms. am. assert (opp (opp' a) = opp' (opp' a)). uf opp. ap (Y_if H1). reflexivity. rw H2. rw opp'_opp'. tv. am. assert (opp a = a). uf opp. ap (Y_if_not H). tv. rw H0. uf opp. ap (Y_if_not H). tv. Qed.
imports: Arith universe