proposition: Lemma SplitL_resp_Qeq : forall (s t:StepF) (a b:OpenUnit), a == b -> StepF_Qeq s t -> StepF_Qeq (SplitL s a) (SplitL t b).
proof: Proof. intros s t a b H H0. apply StepF_Qeq_trans with (Mirror (Mirror (SplitL s a))); auto with *. apply StepF_Qeq_trans with (Mirror (SplitR (Mirror s) (OpenUnitDual a))). apply Mirror_resp_Qeq. apply MirrorSplitL_Qeq; auto with *. apply StepF_Qeq_trans with (Mirror (SplitR (Mirror t) (OpenUnitDual b))). apply Mirror_resp_Qeq. apply SplitR_resp_Qeq; auto with *. simpl; rewrite -> H; reflexivity. apply StepF_Qeq_trans with (Mirror (Mirror (SplitL t b))); auto with *. apply Mirror_resp_Qeq. apply StepF_Qeq_sym. apply MirrorSplitL_Qeq; auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields