(P : nat -> Type) (H : forall x, P x.+1) : forall x (l : 0 < x), P x. Proof. intros x l. destruct x. 1: contradiction (lt_irrefl _ l). apply H. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids