{z w : Pos} : x1 z <> x0 w := x0_neq_x1 o symmetry _ _. Global Instance decpaths_pos : DecidablePaths Pos. Proof. intros n; induction n as [|zn|on]; intros m; induction m as [|zm|om]. + exact (inl idpath). + exact (inr xH_neq_x0). + exact (inr xH_neq_x1). + exact (inr x0_neq_xH). + destruct (IHzn zm) as [p|q]. - apply inl, ap, p. - apply inr; intro p. by apply q, x0_inj. + exact (inr x0_neq_x1). + exact (inr x1_neq_xH). + exact (inr ). + destruct (IHon om) as [p|q]. - apply inl, ap, p. - apply inr; intro p. by apply q, x1_inj. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable