fact: Fixpoint rClosed_decb' n u : bool:= match u with | rApp s t => andb (rClosed_decb' n s) (rClosed_decb' n t) | rVar x => negb (leb n x) | rConst x => true | rLam s =>rClosed_decb' (S n) s | rRho s =>rClosed_decb' (S n) s end.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd