proposition: Lemma Arepl_mor (F F' : Acz -> Acz) s s' u : fres Aeq F -> fres Aeq F' -> (forall s, Aeq (F s) (F' s)) -> Aeq s s' -> Ain u (Arepl F s) -> Ain u (Arepl F' s').
proof: Proof. intros H1 H2 H3 H4 H5. apply AreplAx; trivial. apply AreplAx in H5 as [y H]; trivial. exists y. now rewrite <- H3, <- H4. Qed.
imports: Setoid Morphisms