proposition: Lemma Acc_symprod_inv x y : Acc Symprod (x,y) -> Acc leA x /\ Acc leB y.
proof: Proof. intros. split. eapply Acc_symprod_invl. apply H. eapply Acc_symprod_invr. apply H. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)