fact: Definition sorted_evar (s: Sort) : forall T : s, t T := match s with | Propₛ => fun T:Prop => M.evar T | Typeₛ => fun T:Type => M.evar T end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)