proposition: Lemma Asep_proper' (P P' : Acz -> Prop) s s' : cres Aeq P -> cres Aeq P' -> (forall s, P s <-> P' s) -> Aeq s s' -> Aeq (Asep P s) (Asep P' s').
proof: Proof. intros H1 H2 H3 H4. apply Aeq_ext; intros z Z. - apply (Asep_mor H1 H2 H3 H4); assumption. - apply (@Asep_mor P' P s' s); firstorder. Qed.
imports: Setoid Morphisms