proposition: Lemma isrefleqh {X : UU} (is : isdeceq X) : isrefl (eqh is).
proof: Proof. intros. unfold eqh. unfold booleq. intro x. induction (is x x) as [ e | ne ]. - simpl. apply idpath. - induction (ne (idpath x)). Defined.
imports: UniMath.Foundations.Propositions