proposition: Lemma AsepAx (P : Acz -> Prop) s t : cres Aeq P -> Ain t (Asep P s) <-> Ain t s /\ P t.
proof: Proof. intros HP. split; intros H; destruct s as [A f]. - destruct H as [[a PA]H]. split; eauto. now exists a. - destruct H as [[a H]PY]. assert (PA : P (f a)) by now apply (HP t). now exists (exist _ a PA). Qed.
imports: Setoid Morphisms