proposition: Lemma fin_branch : rules_preserve_vars R -> finitely_branching (red R).
proof: Proof. unfold finitely_branching. intros. exists (reducts x). split_all. apply reducts_complete; hyp. apply reducts_correct. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)