fact: Definition denoteComp (phi : nat -> term) :rComp -> Comp:= fix denoteComp s := match s with | rCompVar x => CompVar x | rCompApp s t => (denoteComp s) (denoteComp t) | rCompClos s A => CompClos (denoteTerm phi s) (map denoteComp A) end.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd