fact: Fixpoint aIn {A T} (v : M A) (args : args_for T) : Type := match args with | an_arg A' B' arg args => ({ pf : A' = A | eq_rect A' M arg A pf = v} + @aIn _ _ v args)%type | noargs T => False end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations