Require Import algoRun.
Require Import ZArith.

Definition eqOp := normalize.Eq.
Extraction "run.ml" run checkTracef zero Pos.of_succ_nat eqOp.