{A : Type} {x : A} (p : x = x) (n : Pos) : loopexp_pos p^ n = (loopexp_pos p n)^. Proof. revert n. srapply pos_peano_ind; cbn; trivial. unfold loopexp_pos. intros n q. rewrite 2 pos_peano_ind_beta_pos_succ, q. refine ((inv_pp _ _)^ @ _). apply ap. clear q. revert n. srapply pos_peano_ind; cbn; trivial. intros n q. by rewrite pos_peano_ind_beta_pos_succ, concat_p_pp, q. Qed.
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.