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