proposition: Lemma transport_r_trans (A : Type) (B : A -> Type) : forall (a0 a1 a2 : A) (x : B a2) (p : a0 = a1) (q : a1 = a2), transport_r B p (transport_r B q x) = transport_r B (eq_trans p q) x.
proof: Proof. intros a0 a1 a2 x p q; destruct p, q; reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic