proposition: Lemma StepF_Qeq_refl : forall (s: StepF), StepF_Qeq s s.
proof: Proof. induction s; simpl; auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields