fact: Fixpoint range_of (T : TypeCode) : SimpleTypeCode := match T with | carrow A B => range_of B | csimple T => T end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations