proposition: Lemma top_reducts_complete : forall t u R, rules_preserve_vars R -> hd_red R t u -> In u (top_reducts R t).
proof: Proof. induction R; intros; redtac. hyp. simpl in lr. assert (h0 : rules_preserve_vars R). eapply rules_preserve_vars_incl. 2: apply H. apply incl_tl. refl. split_all. 2:{ simpl. assert (h1 : hd_red R t u). subst. apply hd_red_rule. hyp. case (top_reduct t a). right. apply IHR; hyp. apply IHR; hyp. } subst a. simpl. unfold top_reduct. simpl. case_eq (matches l t). intros t0 H0. ded (matches_correct H0). left. subst u. apply sub_eq. intros. eapply subeq_inversion. rewrite xl in H1. apply H1. unfold rules_preserve_vars in H. unfold List.incl in H. eapply H. simpl. auto. hyp. intro H0. symmetry in xl. ded (matches_complete xl). congruence. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)