proposition: Lemma denoteTerm_correct phi s: Proc phi -> deClos (denoteComp phi s) = denoteTerm phi (rDeClos s).
proof: Proof. intros pp. unfold denoteComp, rDeClos. pattern s. apply rComp_ind_deep;intros;simpl;try congruence. - rewrite rSubstList_correct;auto. f_equal. rewrite !map_map. now apply map_ext'. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd