fact: Definition onelevelG (T : TypeCode) : Type := match T with | csimple T' => onelevel T' | _ => Empty_set end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations