proposition: Lemma symb_ord_img_rec_incl : forall Rc1 Rc2 R f, Rc1 [= Rc2 -> symb_ord_img_rec R Rc1 f [= symb_ord_img_rec R Rc2 f.
proof: Proof. intros Rc1. induction Rc1. simpl; intros. apply incl_nil. intros. simpl. case_eq (root_eq f (lhs a) && Inb (@eq_rule_dec _) a R); intro H0. 2:{ apply IHRc1. apply incl_cons_l_incl with (x := a); auto. } apply incl_app. intros g Hg. rewrite andb_true_iff in H0. destruct H0. apply symb_ord_img_recP2 with (a := a); auto. apply (Inb_true (@eq_rule_dec _) _ _ H1). apply (incl_cons_l_in H). apply IHRc1. apply incl_cons_l_incl with (x := a); auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)