proposition: Lemma ap_iter {A B C} (f : A -> B) (g : B -> C) (x y : A) (e : x = y) : Top.ap g (Top.ap f e) = Top.ap (fun x => g (f x)) e.
proof: Proof. revert y e. refine (Top.J _ _). reflexivity. Qed.
imports: Equations(Equations)