proposition: Lemma trans_union : forall a b, trans_clos (union _ R1 R2) a b <-> union _ (trans_clos R1) (compose_rel (refl_trans_clos R1) (trans_clos (compose_rel R2 (refl_trans_clos R1)))) a b.
proof: Proof. intros a b; split. intro H; induction H as [x y H1 | x y z H1 Hn]. destruct H1 as [H1 | H1]. left; apply t_step; assumption. right; apply Comp with x. apply r_step. apply t_step. apply Comp with y; trivial. apply r_step. destruct H1 as [H1 | H2]; destruct IHHn as [IHHn | IHHn]. left; apply t_trans with y; trivial. right; inversion IHHn as [x' y' z' K1 K2]; subst x' z'; clear IHHn. apply Comp with y'. inversion K1 as [y1 | y1 y2 K1']; clear K1. subst y1 y'; apply t_clos; apply t_step; trivial. subst y1 y2; apply t_clos; apply t_trans with y; trivial. trivial. right. apply Comp with x. apply r_step. apply t_step; apply Comp with y; trivial. apply t_clos; trivial. right; inversion IHHn as [x' y' z' K1 K2]; subst x' z'; clear IHHn. apply Comp with x. apply r_step. apply t_trans with y'; trivial. apply Comp with y; trivial. intros [H | H]. apply trans_incl with R1; trivial. intros; left; trivial. inversion H as [x' y' z' K1 K2]; clear H; subst x' z'. inversion K1 as [y1 | y1 y2 K1']; clear K1. subst y1 y'. apply trans_clos_is_clos. apply trans_incl with (compose_rel R2 (refl_trans_clos R1)); trivial. clear a b K2; intros a b K2. inversion K2 as [x' y' z' K1 K2']; clear K2; subst x' z'. inversion K2' as [y1 | y1 y2 K2'']; clear K2'. subst y1 y'; apply t_step; right; trivial. subst y1 y2. apply t_trans with y'. right; trivial. apply trans_incl with R1; trivial. intros; left; trivial. subst y1 y2. apply trans_clos_is_trans with y'. apply trans_incl with R1; trivial. intros; left; trivial. apply trans_clos_is_clos. apply trans_incl with (compose_rel R2 (refl_trans_clos R1)); trivial. clear a b y' K1' K2; intros a b K2. inversion K2 as [x' y' z' K1 K2']; clear K2; subst x' z'. inversion K2' as [y1 | y1 y2 K2'']; clear K2'. subst y' y1. left; right; trivial. subst y1 y2. right with y'. right; trivial. apply trans_incl with R1; trivial. intros; left; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)