proposition: Lemma Acc_symprod_fst x : Acc Symprod x -> Acc leA (fst x).
proof: Proof. induction 1. destruct x. simpl. apply Acc_intro. intros. ded (H0 (y,b)). apply H2. apply left_sym. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)