proposition: Lemma structure_opp : forall a, structure (opp a) = structure 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. rww structure_opp'. assert (opp a = a). uf opp. ap (Y_if_not H). tv. rww H0. Qed.
imports: Arith universe