proposition: Lemma env_sub_disjoint : forall E F, (forall p, E |= p :! \/ F |= p :!) -> E [-] F = E.
proof: Proof. induction E; auto. intros F H. simpl. destruct a; destruct F; trivial. destruct o; trivial. destruct (H 0); destruct H0; try_solve. rewrite IHE; trivial. intro p; exact (H (S p)). rewrite IHE; trivial. intro p; exact (H (S p)). Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)