fact: Definition polynormalize {T} (term : polyTerm T) : polyTerm T := fun var => normalize (term _).
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations