proposition: Lemma AreplAx F s u : fres Aeq F -> Ain u (Arepl F s) <-> exists t, Ain t s /\ Aeq u (F t).
proof: Proof. intros HF. split; intros H; destruct s as [A f]. - destruct H as [a H]. exists (f a). split; trivial. apply Ain_Asup. - destruct H as [z[[a H] Z]]. exists a. apply HF in H; try now exists a. now rewrite Z, H. Qed.
imports: Setoid Morphisms