proposition: Lemma ap_ap2 {A B C D} {x y : A} {x' y' : B} {g : A -> B -> C} {f : C -> D} {p : x = y} {q : x' = y'} : ap f (ap2 g p q) = ap2 (fun x y => f (g x y)) p q.
proof: Proof. now destruct p, q; cbn. Qed.
imports: Equations(Equations)