proposition: Lemma StepF_Qeq_sym : forall (s t: StepF), StepF_Qeq s t -> StepF_Qeq t s.
proof: Proof. induction s; induction t; try contradiction; simpl; auto with *. intros [H0 [H1 H2]]. repeat split; eauto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields