fact: Definition overlay (R : relation term) := forall l1 r1 l2 r2 sigma tau, R r1 l1 -> R r2 l2 -> forall f l p, subterm_at_pos l1 p = Some (Term f l) -> apply_subst sigma (Term f l) = apply_subst tau l2 -> p = nil.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)