proposition: Lemma Mirror_resp_Qeq : forall (s t:StepF), StepF_Qeq s t -> StepF_Qeq (Mirror s) (Mirror t).
proof: Proof. induction s; induction t; intros Hst; simpl in *; try assumption; try contradiction. destruct Hst as [Ho [Hst1 Hst2]]. repeat split. rewrite -> Ho; reflexivity. apply IHs2; assumption. apply IHs1; assumption. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields