fact: Definition StFJoin (X : RSetoid):(StepFS (StepFS X))-->(StepFS X):= (flip (@StFBind (StepFS X) X) (@id (StepFS X))).
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics