proposition: Lemma Ap_composition_Qeq : forall X Y Z (a:StepF (Y->Z)) (b:StepF (X->Y)) (c:StepF X), StepF_Qeq (constStepF (@compose X Y Z) <@> a <@> b <@> c) (a <@> (b <@> c)).
proof: Proof. induction a. simpl. induction b. simpl. induction c. auto. repeat split; auto. intros c. simpl in *. destruct (Split c o). repeat split; auto. intros b c. simpl in *. do 2 apply Split_ind. simpl. apply Split_ind. repeat split; eauto. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields