fact: Definition ap2 : forall {A B C : Type} {a a' : A} {b b' : B} (f : A -> B -> C), a = a' -> b = b' -> f a b = f a' b' := fun A B C a a' b b' f e1 e2 => match e1 with | idpath => match e2 with | idpath => idpath end end.
imports: Coq(ssreflect) HoTT(HoTT) Hierarchy