fact: Definition are_connected dpR R uv' uv := exists sigma, exists sigma', match uv, uv' with | (u,v), (u', v') => dpR v u /\ dpR v' u' /\ match (apply_subst sigma' u'), (apply_subst sigma v) with | Term g lu', Term f lv => f = g /\ refl_trans_clos (one_step_list (one_step R)) lu' lv | _, _ => False end end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)