proposition: Lemma symb_ord_img_incl : forall Rc R f g, R [= Rc -> symb_ord R f g -> In g (symb_ord_img_rec R Rc f).
proof: Proof. intros. apply symb_ord_img_rec_incl with (Rc1 := R); auto. destruct H0 as [a [H0 [H1 H2]]]. apply symb_ord_img_recP2 with (a := a); auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)