proposition: Lemma occurs_dec : forall a T, {occurs a T}+{~occurs a T}.
proof: Proof. intro a. induction T; simpl. apply eq_dec. destruct IHT1. fo. destruct IHT2. fo. right. fo. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)