mir-ikbch

Require Import List PeanoNat.
Import ListNotations.
Set Universe Polymorphism.

Set Implicit Arguments.

Inductive t (eff : Type -> Type) (a : Type) :=
| Pure : a -> t eff a
| Eff : forall T, eff T -> (T -> t eff a) -> t eff a.

mir-ikbch

Require Import List PeanoNat Arith Morphisms Setoid.
Import ListNotations.

Set Implicit Arguments.

Ltac optimize db :=
  eexists; intros;
  match goal with
    |- ?X = ?Y =>
    let P := fresh in