fact: Definition Min R (f : nat -> term) := forall i x, subterm x (f i) -> forall g, g 0 = x -> ~IS R g.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)