proposition: Theorem wf_union : commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
proof: Proof. unfold well_founded. intros. apply Acc_union; auto with sets. Qed.
imports: Relation_Operators Relation_Definitions Transitive_Closure