proposition: Lemma glue_resp_StepF_eq:forall (x x' y y':StepF X) o, (x==x')->(y==y')-> (glue o x y)==(glue o x' y').
proof: Proof. intros. unfold StepF_eq. rewrite MapGlue. rewrite ApGlueGlue. split; assumption. 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