fact: Definition interp_Term {T} (t : Term interp_TypeCode T) : interp_TypeCode T := interp_Term_gen (@interp_RLiteralTerm) t.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Common.List.Operations