{A : Type} {x : A} (p : x = x) (a : Pos) : loopexp_pos p a @ p = p @ loopexp_pos p a. Proof. induction a as [|a aH] using pos_peano_ind; trivial. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. change ((loopexp_pos p a @ p) @ p = p @ (loopexp_pos p a @ p)). by rewrite concat_p_pp, aH. 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.