{A : Type} {x : A} (p : x = x) (z : Int) : loopexp p z.+1 = p @ loopexp p z. Proof. lhs nrapply loopexp_succ_r. induction z as [|z|z]. - nrapply concat_1p_p1. - rewrite loopexp_succ_r. rhs nrapply concat_p_pp. f_ap. - rewrite loopexp_pred_r. lhs nrapply concat_pV_p. rhs nrapply concat_p_pp. by apply moveL_pV. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.