proposition: Lemma loopexp_pos_concat {A : Type} {x : A} (p : x = x) (a : Pos) : loopexp_pos p a @ p = p @ loopexp_pos p a.
proof: 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.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv