fact: Variable UIR : forall t s s', inner R t -> axiom R s t -> axiom R s' t -> s = s'.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)