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