proposition: Lemma expandDenote phi s: Proc phi -> denoteTerm phi s = deClos (denoteComp phi (rCompClos s [])).
proof: Proof. intros pp. rewrite (denoteTerm_correct _ pp). simpl. rewrite rSubstList_correct;auto. simpl. now rewrite substList_nil. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd