proposition: Lemma int_mon : forall T, (pos a T -> int I T [<=] int J T) /\ (neg a T -> int J T [<=] int I T).
proof: Proof. induction T; simpl_pos. destruct (eq_dec s a). subst s. fo. fo. destruct IHT1 as [i1 i2]. destruct IHT2 as [j1 j2]. split; intros [h1 h2]; apply arr_incl; fo. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)