proposition: Lemma R1_R2_case : forall (s t : term), Interp_dom R1 R2 s -> rwr (@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 t_R_s; induction t_R_s; subst. apply R1_R2_case_one_step; trivial. destruct (IHt_R_s Is) as [s' [t' [Hs' [Ht' t'_R_s']]]]. assert (It2 : Interp_dom R1 R2 y). apply interp_dom_R1_R2_rwr with z; trivial. destruct (R1_R2_case_one_step y x It2 H) as [s'' [t'' [Hs'' [Ht'' t''_R_s'']]]]. exists s'; exists t''; split; trivial. split; trivial. apply trans_clos_is_trans with s''; trivial. rewrite (interp_unicity _ It2 _ _ Hs'' Ht'); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)