proposition: Lemma MirrorAp_Qeq (X Y: Type) : forall (f: StepF (X -> Y)) s, StepF_Qeq (Mirror (f <@> s)) ((Mirror f) <@> (Mirror s)).
proof: Proof. induction f; intros s. simpl. rewrite MirrorMap. auto with *. rewrite ApGlue. change (StepF_Qeq (glue (OpenUnitDual o) (Mirror (f2 <@> (SplitR s o))) (Mirror (f1 <@> (SplitL s o)))) ((glue (OpenUnitDual o) (Mirror f2) (Mirror f1)) <@> (Mirror s))). rewrite ApGlue. repeat split; auto with *. eapply StepF_Qeq_trans. apply IHf2. apply Ap_resp_Qeq; auto with *. apply MirrorSplitR_Qeq. reflexivity. eapply StepF_Qeq_trans. apply IHf1. apply Ap_resp_Qeq; auto with *. apply MirrorSplitL_Qeq. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields