proposition: Lemma Asep_mor (P P' : Acz -> Prop) s s' t : cres Aeq P -> cres Aeq P' -> (forall s, P s <-> P' s) -> Aeq s s' -> Ain t (Asep P s) -> Ain t (Asep P' s').
proof: Proof. intros H1 H2 H3 H4 H5. apply AsepAx; trivial. rewrite <- H3, <- H4. apply AsepAx; trivial. Qed.
imports: Setoid Morphisms