fact: Definition ahd {A B} (af : args_for (A --> B)) : M A := match af in args_for T return match T with | carrow A B => M A | _ => unit end with | an_arg _ _ arg _ => arg | _ => tt end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations