fact: Fixpoint apply_meaning_helper {P} (af : arg_meanings_for P) : forall (f : normalized_of P), normalized_of (range_of P) := match af in args_for _ P return normalized_of P -> normalized_of (range_of P) with | an_arg _ _ arg args => fun f => @apply_meaning_helper _ args (f arg) | noargs _ => fun v => v end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations