{A : Type} {x : A} (p : x = x) (z : BinInt) : (x = x) := match z with | neg n => loopexp_pos p^ n | zero => 1 | pos n => loopexp_pos p n end.
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.