proposition: Lemma transportD_compose {A A'} B {x x' : A} (C : forall x : A', B x -> Type) (f : A -> A') (p : x = x') y (z : C (f x) y) : transportD (B o f) (C oD f) p y z = transport (C (f x')) (transport_compose B f p y)^ (transportD B C (ap f p) y z).
proof: Proof. destruct p; reflexivity. Defined.
imports: Basics.Overture Basics.Tactics