proposition: Lemma Ap_homomorphism : forall X Y (f:X->Y) (a:X), (constStepF f <@> constStepF a) = (constStepF (f a)).
proof: Proof. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields