proposition: Lemma env_sub_ln : forall E E' x, E |= x :! -> E [-] E' |= x :!.
proof: Proof. induction E; destruct E' as [|a' E']; intros; trivial. destruct a; trivial. inversion H; destruct x; destruct a; destruct a'; simpl in *; solve [ discr | auto | unfold VarUD; destruct (IHE E' x); auto ]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)