proposition: Lemma assoc4 {X : UU} (opp : binop X) (isa : isassoc opp) : ∏ w x y z : X, opp (opp (opp w x) y) z = opp (opp w (opp x y)) z.
proof: Proof. intros. repeat rewrite isa; exact (idpath _). Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions