proposition: Lemma ApowerAx s t : Ain t (Apower s) <-> ASubq t s.
proof: Proof. split; intros H; destruct s as [A f]. - destruct H as [P H]. intros u Z. apply Aeq_ASubq in H. destruct (H u Z) as [[a PA] I]. now exists a. - exists (fun a => Ain (f a) t). apply Aeq_ext; intros z Z. + destruct t as [B g], Z as [b H1]. destruct (H (g b) (Ain_Asup g b)) as [a J]. assert (H2: Ain (f a) (Asup B g)) by (exists b; auto). exists (exist _ a H2). eauto. + destruct Z as [[a YA] H1 % Aeq_sym]. now apply (Ain_mor H1 (t:=t)). Qed.
imports: Setoid Morphisms