proposition: Lemma symb_ord_dec : forall R, rel_dec (symb_ord R).
proof: Proof. intros R a b. case_eq (Inb (@eq_symb_dec _) b (symb_ord_img R a)); intro H. left. rewrite <- symb_ord_imgP. apply (Inb_true (@eq_symb_dec _) _ _ H). right. intro. rewrite <- symb_ord_imgP in H0. apply (Inb_false (@eq_symb_dec _) _ _ H); auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)