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