proposition: Lemma env_eq_cons : forall a b E E', a = b -> E [=] E' -> a :: E [=] b :: E'.
proof: Proof. intros; split; rewrite H. inversion H0. destruct b. fold (s [#] E); fold (s [#] E'); apply env_subset_cons; trivial. apply env_subset_cons_none; trivial. inversion H0. destruct b. fold (s [#] E); fold (s [#] E'); apply env_subset_cons; trivial. apply env_subset_cons_none; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)