proposition: Lemma concat2_ap_ap {A B : Type} {x' y' z' : B} (f : A -> (x' = y')) (g : A -> (y' = z')) {x y : A} (p : x = y) : (ap f p) @@ (ap g p) = ap (fun u => f u @ g u) p.
proof: Proof. by path_induction. Defined.
imports: Basics.Overture Basics.Tactics