proposition: Lemma Acc_union : commut A R1 R2 -> (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
proof: Proof. induction 3 as [x H1 H2]. apply Acc_intro; intros. elim H3; intros; auto with sets. cut (clos_trans A R1 y x); auto with sets. cut (Acc (clos_trans A R1) y); [ intro H'; elim H' | ]; intros. - apply Acc_intro; intros. elim H8; intros. + apply H6; auto with sets. apply t_trans with x0; auto with sets. + elim strip_commut with x x0 y0; auto with sets; intros. apply Acc_inv_trans with x1; auto with sets. unfold union. elim H11; auto with sets; intros. apply t_trans with y1; auto with sets. - apply (Acc_clos_trans A). apply Acc_inv with x; auto with sets. apply H0. apply Acc_intro; auto with sets. Qed.
imports: Relation_Operators Relation_Definitions Transitive_Closure