fact: Fixpoint map_args_for {T} (args : args_for M T) : args_for N T := match args in args_for _ T return args_for _ T with | an_arg A B arg args => an_arg (F arg) (map_args_for args) | noargs T => noargs end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations