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. induction T; simpl. fo. intro h. rewrite IHT1, IHT2. refl. intuition. intuition. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)