proposition: Lemma distinct_pairs_and_app_cons : forall A R xs p ys l, l = (xs ++ p :: ys) -> distinct_pairs_and (A:=A) R l -> distinct_pairs_and R (xs ++ ys).
proof: Proof. Proof using. induction xs; intros; subst; simpl in *; intuition eauto. Qed.
imports: Verdi(Verdi)