proposition: Lemma Mirror_eq_Mirror : forall (s t : StepF X), Mirror s == Mirror t <-> s == t.
proof: Proof. induction s. induction t; simpl. reflexivity. change (constStepF x == (Mirror t2) /\ constStepF x == (Mirror t1) <-> constStepF x == t1 /\ constStepF x == t2). tauto. intros t. rewrite MirrorGlue. split; apply (@glue_eq_ind X); intros H0 H1. apply glue_StepF_eq. rewrite <- IHs1. eapply StepF_eq_resp_Qeq;[| |apply H1]; auto with *. apply StepF_Qeq_sym. apply MirrorSplitL_Qeq; auto with *. rewrite <- IHs2. eapply StepF_eq_resp_Qeq;[| |apply H0]; auto with *. apply StepF_Qeq_sym. apply MirrorSplitR_Qeq; auto with *. apply glue_StepF_eq. apply StepF_eq_resp_Qeq with (Mirror s2) (Mirror (SplitR t o)); auto. apply MirrorSplitR_Qeq; apply Qeq_refl. rewrite -> IHs2. assumption. apply StepF_eq_resp_Qeq with (Mirror s1) (Mirror (SplitL t o)); auto. apply MirrorSplitL_Qeq; apply Qeq_refl. rewrite -> IHs1. assumption. 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