proposition: Lemma AupairAx s t u : Ain u (Aupair s t) <-> Aeq u s \/ Aeq u t.
proof: Proof. split; intros H. - destruct H as [[] H]; auto. - destruct H as [H|H]; [now exists true | now exists false]. Qed.
imports: Setoid Morphisms