proposition: Lemma Acc_symprod_snd x : Acc Symprod x -> Acc leB (snd x).
proof: Proof. induction 1. destruct x. simpl. apply Acc_intro. intros. ded (H0 (a,y)). apply H2. apply right_sym. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)