proposition: Lemma symb_ord_img_recP1 : forall Rc R f g, In g (symb_ord_img_rec R Rc f) -> symb_ord R f g.
proof: Proof. intro Rc; elim Rc; simpl; intros; try tauto. case_eq (root_eq f (lhs a) && Inb (@eq_rule_dec _) a R); intro H1; rewrite H1 in H0. 2: apply (H R f g H0). rewrite andb_true_iff in H1; destruct H1. destruct (in_app_or H0). exists a; split; auto. apply (Inb_true (@eq_rule_dec _) _ _ H2). apply (H R f g H3). Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)