fact: Fixpoint reify {T} : normalized_of T -> Term var T := match T return normalized_of T -> Term var T with | csimple _ => fun x => x | carrow A B => fun f => RLambda (fun x => reify (f (reflect (RVar x)))) end with reflect {T} : Term var T -> normalized_of T := match T return Term var T -> normalized_of T with | csimple _ => fun x => x | carrow A B => fun e x => reflect (RApp e (reify x)) end.
imports: Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.Syntactify Fiat.Common Fiat.Common.NatFacts Fiat.Common.List.Operations