Definition loop_power_nat {Y} {y:Y} (l:y = y) (n:nat) : y = y. Proof. intros. induction n as [|n p]. { exact (idpath _). } { exact (p@l). } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.