proposition: Lemma int_equiv' : forall I J T, (forall a, occurs a T -> I a [=] J a) -> int I T [<=] int J T.
proof: Proof. intros I J T IJ. rewrite (int_equiv _ _ T IJ). refl. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)