{x y} : x <= y -> y <= x -> x = y. Proof. intros p q. destruct p. 1: reflexivity. destruct x; [inversion q|]. apply leq_pred' in q. contradiction (lt_irrefl _ (leq_trans p q)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids