proposition: Lemma env_subset_single : forall A x E, E |= x := A -> envSubset (copy x None ++ A [#] EmptyEnv) E.
proof: Proof. intros; intros w B D. destruct (varDecl_single x A D). rewrite <- H0; rewrite <- H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)