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