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