proposition: Lemma reducts_fun : forall f ts, reducts (Fun f ts) = top_reducts R (Fun f ts) ++ reducts_vec f ts ts (Nat.le_refl (arity f)).
proof: Proof. intros. simpl. rewrite <- fix_reducts_vec. refl. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)