proposition: Lemma emptyEnv_absurd : forall a E P, emptyEnv (Some a :: E) -> P.
proof: Proof. intros. exfalso. assert ((Some a :: E) |= 0 := a). auto with terms. destruct (H 0); try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)