proposition: Lemma Acc_swapprod : forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
proof: Proof. induction 1 as [x0 _ IHAcc0]; intros H2. cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)). - clear IHAcc0. induction H2 as [x1 _ IHAcc1]; intros H4. cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)). + clear IHAcc1. intro. apply Acc_intro. destruct y; intro H5. inversion_clear H5. * inversion_clear H0; auto with sets. * apply swap_Acc. inversion_clear H0; auto with sets. + intros. apply IHAcc1; auto with sets; intros. apply Acc_inv with (y0, x1); auto with sets. apply sp_noswap. apply right_sym; auto with sets. - auto with sets. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image