fact: Definition exfalso_option_none_some : forall (T : Type) (A : Type) (a : A), None = Some a -> T := fun T A a e => match e in @paths _ _ t return match t with | None => Unit | Some _ => T end with | idpath => tt end.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy