proposition: Lemma env_sum_ln_rn : forall E1 E2 x, E1 |= x :! -> E2 |= x :! -> E1 [+] E2 |= x :!.
proof: Proof. induction E1; destruct E2 as [|a' E2]; trivial. destruct x. inversion 1; inversion 1; destruct a'; auto. unfold VarUD; inversion 1; inversion 1; destruct a'; simpl in *; apply IHE1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)