proposition: Lemma first_id : forall a z, first (a:=a) (b:=a) (z:=z) id = id.
proof: Proof. unfold first. intros a z. extensionality x. destruct x; auto. Qed.
imports: Hask.Prelude Hask.Ltac Hask.Control.Monad Hask.Control.Monad.State Hask.Control.Monad.Trans.Class FunctionalExtensionality