fact: Definition pair_inj1 A B (a1 a2 : A) (b1 b2 : B) : (a1, b1) = (a2, b2) -> a1 = a2 := fun e => match e in @paths _ _ (a, b) return _ = a with | @idpath _ _ => @idpath _ a1 end.
imports: Coq(ssreflect) HoTT(HoTT) Hierarchy