proposition: Lemma SplitRAp_Qeq (X Y:Type) : forall (f: StepF (X -> Y)) s o, StepF_Qeq (SplitR (f <@> s) o) ((SplitR f o) <@> (SplitR s o)).
proof: Proof. intros f s o. eapply StepF_Qeq_trans. apply StepF_Qeq_sym. apply MirrorMirror. eapply StepF_Qeq_trans;[|apply MirrorMirror]. apply Mirror_resp_Qeq. eapply StepF_Qeq_trans;[|apply StepF_Qeq_sym; apply MirrorAp_Qeq]. eapply StepF_Qeq_trans. apply MirrorSplitR_Qeq. reflexivity. eapply StepF_Qeq_trans. apply SplitL_resp_Qeq. reflexivity. apply MirrorAp_Qeq. eapply StepF_Qeq_trans. apply SplitLAp_Qeq. apply StepF_Qeq_sym. apply Ap_resp_Qeq; apply MirrorSplitR_Qeq; reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields