proposition: Lemma Aeq_sym s t : Aeq s t -> Aeq t s.
proof: Proof. revert t. induction s as [A f IH]. intros [B g]. simpl. intros [H1 H2]. split. - intros b. destruct (H2 b) as [a H3]. exists a. now apply IH. - intros a. destruct (H1 a) as [b H3]. exists b. now apply IH. Qed.
imports: Setoid Morphisms