proposition: Lemma deClos_validEnv A : validEnv A -> validEnv' (map deClos A).
proof: Proof. intros vA. induction A;simpl. - unfold validEnv'. simpl. tauto. - rewrite validEnv'_cons. apply validEnv_cons in vA as [ca cA]. split;auto. apply deClos_valComp; auto. Qed.