proposition: Lemma StepF_eq_sym :forall x y: StepF X, x == y -> y == x.
proof: Proof. intros x y. revert x. induction y. unfold StepF_eq. simpl. intro x0. induction x0. unfold StepFfoldProp. simpl. intros. symmetry; assumption. simpl. unfold StepFfoldProp; simpl; intuition; auto with *. intros x H. assert (H0:=(SplitL_resp_Xeq _ _ o H)). rewrite SplitLGlue in H0. assert (H1:=(SplitR_resp_Xeq _ _ o H)). rewrite SplitRGlue in H1. apply glue_StepF_eq;auto with *. 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