proposition: Lemma SplitLMap : forall (X Y : RSetoid) (x : StepF X) (a : OpenUnit) (f : X --> Y), SplitL (f ^@> x) a = f ^@> (SplitL x a).
proof: Proof. intros X Y x a f. unfold Ap. simpl. rewrite SplitLMap. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields