proposition: Lemma Ap_identity : forall X (a:StepF X), constStepF (fun x => x) <@> a = a.
proof: Proof. induction a. reflexivity. simpl in *. rewrite IHa1. rewrite IHa2. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields