proposition: Lemma isapropislunit {X : hSet} (opp : binop X) (un0 : X) : isaprop (islunit opp un0).
proof: Proof. apply impred. intro x. simpl. apply (setproperty X). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions