ew.v

Lemma ap_pres_comp : forall {t u} (pu : parser (t -> u)) (pv : parser (t -> t)) pw,
    ((ret compose <*> pu) <*> pv) <*> pw = pu <*> (pv <*> pw).
Proof.
  intros.
  unfold ap.
  unfold flatmap.
  extensionality x.
  simpl.
  destruct (pu x).
  destruct p.
  unfold ret.
  destruct (pv s).
  destruct pw.
  assumption.
  destruct p.
  destruct (pw s0).
  destruct p.
  reflexivity.
  reflexivity.
  destruct p.
  destruct (pw s0).
  destruct p.
  reflexivity.
  reflexivity.
  reflexivity.
  reflexivity.
Qed.