{A : Type} {x : A} (p : x = x) (n : Pos) : (x = x). Proof. revert n. srapply pos_peano_ind. + exact p. + intros n q. exact (q @ p). Defined.
Require Import Basics. Require Import Types.Universe. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec. Require Import Spaces.BinInt.Equiv.