proposition: Lemma id_opp : forall a x, ob (opp a) x -> id (opp a) x = flip (id a x).
proof: Proof. ir. assert (axioms a). wr axioms_opp. uh H; ee; am. rw unfold_opp. rww id_opp'. ap ob_is_ob. wrr unfold_opp. am. Qed.
imports: Arith universe