Lemma isaprop_consecutive {X : Poset} (x y : X) : isaprop (consecutive x y). Proof. intros. unfold consecutive. apply isapropdirprod. - apply isapropdirprod. { apply pr2. } simpl. apply isapropneg. - apply impred; intro z. apply isapropneg. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.