proposition: Lemma top_reduct_correct : forall R lr t u, In lr R -> top_reduct t lr = Some u -> hd_red R t u.
proof: Proof. intros R0 lr t u hlr. unfold top_reduct. destruct lr as [l r]. simpl. case_eq (matches l t); intros t0 H. intro H0. ded (matches_correct H). subst. inversion H0. apply hd_red_rule. hyp. discr. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)