proposition: Lemma transport_f_equal (A B : Type) (C : B -> Type) (f : A -> B) (x y : A) (p : x = y) (t : C (f x)) : transport (fun a => C (f a)) p t = transport (fun b => C b) (f_equal f p) t.
proof: Proof. destruct p. reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic