proposition: Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f x)) : transport (fun x => P (f x)) p z = transport P (ap f p) z.
proof: Proof. destruct p; reflexivity. Defined.
imports: Basics.Overture Basics.Tactics