fact: Definition interp_Term_gen_step {T} (t : Term interp_TypeCode T) : interp_TypeCode T := match t in (Term _ T') return interp_TypeCode T' with | RVar T v => v | RLambda A B f => fun x => @interp_Term_gen _ (f x) | RApp A B f x => @interp_Term_gen _ f (@interp_Term_gen _ x) | RLiteralApp c t args => apply_args_for (interp_RLiteralTerm t) (map_args_for (@interp_Term_gen) args) end.
imports: Coq.Strings.String Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Syntactify Fiat.Common.NatFacts Fiat.Common.BoolFacts Fiat.Common.List.Operations