fact: Definition StepFfoldProp : StepF iffSetoid -> Prop := (StepFfold (X:=iffSetoid) (fun x => x ) (fun _ a b => a /\ b )).
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields