proposition: Lemma top_reducts_correct_red : forall t u R, In u (top_reducts R t) -> red R t u.
proof: Proof. intros. ded (top_reducts_correct H). eapply incl_elim. apply hd_red_incl_red. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)