proposition: Theorem polynormalize_correct : forall t (E : polyTerm t), Term_equiv nil (E interp_TypeCode) (E (normalized_of interp_TypeCode)) -> Proper_relation_for _ (interp_Term (E _)) (interp_Term (polynormalize E _)).
proof: Proof. unfold interp_Term, polynormalize, normalize; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.PartialUnfold Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Parsers.Reflective.Morphisms Fiat.Common.List.ListFacts Fiat.Common.Equality