fact: Definition inner_hd_red u v := exists l r s, In (mkRule l r) R /\ u = sub s l /\ v = sub s r /\ innermost u.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)