proposition: Lemma symb_ord_img_rec_cons2 : forall Rc a R f, symb_ord_img_rec R Rc f [= symb_ord_img_rec R (a :: Rc) f.
proof: Proof. intros; simpl. case_eq (root_eq f (lhs a) && Inb (@eq_rule_dec _) a R); intro H. apply incl_appr; refl. refl. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)