fact: Fixpoint args_for_related {T} (args0 : args_for M T) : args_for N T -> Prop := match args0 in args_for _ T return args_for _ T -> Prop with | an_arg A B arg args => fun args1 => R arg (ahd args1) /\ @args_for_related _ args (atl args1) | noargs T => fun args1 => noargs = args1 end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations