proposition: Lemma FB12 : forall s t, one_step (@union _ R1 R2) s t <-> In s (R1_R2_red t).
proof: Proof. intros s t; split. intro s_R_t; rewrite split_rel in s_R_t; unfold R1_R2_red; destruct s_R_t as [s_R1_t | s_R2_t]; apply in_or_app. left; rewrite <- FB1; trivial. right; rewrite <- FB2; trivial. intro s_in_l; unfold R1_R2_red in s_in_l; destruct (in_app_or _ _ _ s_in_l) as [K1 | K2]. rewrite split_rel; left; rewrite FB1; trivial. rewrite split_rel; right; rewrite FB2; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)