proposition: Lemma iseqrel_closure {X : UU} (R : hrel X) : iseqrel (eqrel_closure_hrel R).
proof: Proof. use iseqrelconstr. - intros x y z. apply hinhfun2. apply concat. - intro x. apply hinhpr. apply nil. - intros x y. apply hinhfun. apply reverse_in_closure. Defined.
imports: UniMath.Combinatorics.GraphPaths UniMath.MoreFoundations.Subtypes