proposition: Lemma transport_precompose {A B C} (f : A -> B) (g g' : B -> C) (p : g = g') : transport (fun h : B -> C => g o f = h o f) p 1 = ap (fun h => h o f) p.
proof: Proof. destruct p; reflexivity. Defined.
imports: Basics.Overture Basics.Tactics