fact: Fixpoint normalized_of (T : TypeCode) : Type := match T with | csimple T' => Term var T' | carrow A B => normalized_of A -> normalized_of B end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations