proposition: Lemma SplitLAp_Qeq (X Y:Type) : forall (f: StepF (X -> Y)) s o, StepF_Qeq (SplitL (f <@> s) o) ((SplitL f o) <@> (SplitL s o)).
proof: Proof. induction f; intros. simpl. rewrite SplitLMap; auto with *. rewrite ApGlue. unfold SplitL at 1 3. simpl. destruct (Q_dec o0 o) as [[Ho|Ho]|Ho]. do 2 apply Split_ind. simpl. eapply StepF_Qeq_trans; try assumption. apply IHf1. apply Ap_resp_Qeq; auto with *. apply SplitLSplitL. simpl. field; auto with *. do 2 apply Split_ind. simpl. apply Split_ind. repeat split; auto with *. apply Ap_resp_Qeq; auto with *. apply StepF_Qeq_sym. apply SplitLSplitL. simpl. field; auto with *. eapply StepF_Qeq_trans; try assumption. apply IHf2. apply Ap_resp_Qeq; auto with *. apply SplitLSplitR; simpl; field; auto with *. simpl. apply Ap_resp_Qeq; auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields