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