proposition: Lemma Ap_interchange : forall X Y (f:StepF (X->Y)) (a:X), (f <@> constStepF a) = (constStepF (fun g => g a)) <@> f.
proof: Proof. induction f. reflexivity. intros a. simpl. rewrite IHf1. rewrite IHf2. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields