proposition: Lemma symb_ord_img_recP2 : forall Rc R f g a, In g (def_symbs R (rhs a)) -> In a R -> In a Rc -> root_eq f (lhs a) = true -> In g (symb_ord_img_rec R Rc f).
proof: Proof. intro Rc; elim Rc; intros. inversion H1. destruct (in_inv H2). simpl. subst. rewrite H3, (Inb_intro (@eq_rule_dec _) _ _ H1). simpl. apply in_appl; auto. apply symb_ord_img_rec_cons2. apply (H R f g a0); auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)