fact: Definition goal_type (g : goal gs_open) : t Type := match g with | Metavar s A x => match s as s return stype_of s -> t Type with | Propₛ => fun A => ret (A:Type) | Typeₛ => fun A => ret A end A end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)