proposition: Lemma def_symbs_incl : forall R a t, def_symbs R t [= def_symbs (a :: R) t.
proof: Proof. intros. intro x; unfold def_symbs. rewrite !filter_In; simpl. destruct a as [[] r]; simpl; auto. rewrite orb_true_iff. intro H. destruct H; split; auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)