proposition: Lemma two_arg_paths {A B C:UU} {f : A -> B -> C} {a1 b1 a2 b2} (p : a1 = a2) (q : b1 = b2) : f a1 b1 = f a2 b2.
proof: Proof. intros. induction p. induction q. apply idpath. Defined.
imports: UniMath.Foundations.Preamble