proposition: Lemma Aeq_tra s t u : Aeq s t -> Aeq t u -> Aeq s u.
proof: Proof. revert t u. induction s as [A f IH]. intros [B g] [C h]. simpl. intros [H1 H2] [H3 H4]. split. - intros a. destruct (H1 a) as [b H5]. destruct (H3 b) as [c H6]. exists c. now apply IH with (t := (g b)). - intros c. destruct (H4 c) as [b H5]. destruct (H2 b) as [a H6]. exists a. now apply IH with (t := (g b)). Qed.
imports: Setoid Morphisms