proposition: Lemma symb_ord_cons : forall a R f g, symb_ord R f g -> symb_ord (a :: R) f g.
proof: Proof. intros. destruct H as [h [Hh1 [Hh2 Hh3]]]. exists h. split. apply in_cons; auto. split; auto. unfold def_symbs; simpl. destruct a as [[] r]; simpl; auto. unfold def_symbs in Hh3; rewrite filter_In in Hh3; rewrite filter_In. split; destruct Hh3; auto. rewrite orb_true_iff, H0; right; auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)