{A B} (f : A -> B) {x : A} (p : x = x) (z : BinInt) : ap f (loopexp p z) = loopexp (ap f p) z. Proof. destruct z as [n| |n]; trivial. + cbn. rewrite loopexp_pos_inv, ap_V, loopexp_pos_inv. apply ap. apply ap_loopexp_pos. + apply ap_loopexp_pos. 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.