proposition: Lemma Arepl_proper' (F F' : Acz -> Acz) s s' : fres Aeq F -> fres Aeq F' -> (forall s, Aeq (F s) (F' s)) -> Aeq s s' -> Aeq (Arepl F s) (Arepl F' s').
proof: Proof. intros H1 H2 H3 H4. apply Aeq_ext; intros z Z. - apply (Arepl_mor H1 H2 H3 H4); assumption. - apply (@Arepl_mor F' F s' s); auto. Qed.
imports: Setoid Morphisms