proposition: Lemma R1_R2_case_one_step : forall (s t : term), Interp_dom R1 R2 s -> one_step (@union _ R1 R2) t s -> exists s', exists t', Interp s s' /\ Interp t t' /\ rwr (@union _ R1 (Pi pi V0 V1)) t' s'.
proof: Proof. intros s t Is H. rewrite split_rel in H. destruct H as [H1 | H2]. apply R1_case; trivial. destruct (R2_case s t Is H2) as [s' [t' [Hs' [Ht' H']]]]. exists s'; exists t'; split; trivial. split; trivial. apply rwr_incl with (Pi pi V0 V1); trivial. intros t1 t2 H''; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)