fact: Definition solve_typeclass_or_fail (A : Type) : t A := x <- solve_typeclass A; match x with mSome a => M.ret a | mNone => raise (NoClassInstance A) end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)