fact: Definition chain_min s t := chain s t /\ lforall (SN (red R)) (direct_subterms s) /\ lforall (SN (red R)) (direct_subterms t).
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)