proposition: Lemma Aeq_ext s t : ASubq s t -> ASubq t s -> Aeq s t.
proof: Proof. destruct s as [A f], t as [B g]. intros H1 H2. simpl. split. - intros a. destruct (H1 (f a) (Ain_Asup f a)) as [b H3]. now exists b. - intros b. destruct (H2 (g b) (Ain_Asup g b)) as [a H3]. now exists a. Qed.
imports: Setoid Morphisms