proposition: Lemma env_sumn_ln : forall x E1 E2, E1 [+] E2 |= x :! -> E1 |= x :! .
proof: Proof. induction x. destruct E1; destruct E2; try destruct o0; try_solve. inversion 1; try_solve. destruct E1; destruct E2; try destruct o0; try_solve; revert IHx; unfold VarUD; simpl; intro IHx; gen (IHx E1 E2); tauto. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)