fact: Definition invert_args_for_ex {T} (args : args_for T) : match T return args_for T -> Prop with | csimple T' => fun args => args = noargs | carrow A B => fun args => exists hd tl, args = an_arg hd tl end args.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations