proposition: Lemma Aupair_mor s s' t t' u : Aeq s s' -> Aeq t t' -> Ain u (Aupair s t) -> Ain u (Aupair s' t').
proof: Proof. intros H1 H2 H. apply AupairAx. rewrite <- H1, <- H2. now apply AupairAx in H. Qed.
imports: Setoid Morphisms