proposition: Lemma two_arg_paths_b {A : UU} {B : A -> UU} {C:UU} {f : ∏ a, B a -> C} {a1 b1 a2 b2} (p : a1 = a2) (q : b1 = transportb B p b2) : f a1 b1 = f a2 b2.
proof: Proof. intros. induction p. change _ with (b1 = b2) in q. induction q. apply idpath. Defined.
imports: UniMath.Foundations.Preamble