proposition: Lemma env_subset_cons : forall a E E', envSubset E' E -> envSubset (a [#] E') (a [#] E).
proof: Proof. intros; intros p A. destruct p; fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)