fact: Definition some_inj1 : forall (A : Type) (a1 a2 : A), Some a1 = Some a2 -> a1 = a2 := fun A a1 a2 e => let proj1 (oa : option A) := match oa with | Some a => a | None => a1 end in ap proj1 e.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy