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