proposition: Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
proof: Proof. red. destruct a; intros. apply Acc_swapprod; auto with sets. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image