proposition: Lemma symb_ord_imgP : forall R f g, In g (symb_ord_img R f) <-> symb_ord R f g.
proof: Proof. unfold symb_ord_img; intros; split. apply symb_ord_img_recP1. intros. destruct H as [a [H0 [H1 H2]]]. apply (symb_ord_img_recP2 R R f g a); auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)