proposition: Lemma env_eq_empty_cons : forall E, None :: E [=] EmptyEnv -> E [=] EmptyEnv.
proof: Proof. intros. split. intros p A Ep. set (w := proj1 H (S p) A). unfold VarD in w; simpl in w. set (ww := w Ep); try_solve. apply env_subset_empty. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)