proposition: Theorem implementation : { f : list nat -> Comp nat | forall ls, refine (notInList ls) (f ls) }.
proof: Proof. begin. rewrite notInList_decompose. rewrite listMax_refines. setoid_rewrite increment_refines. monad_simpl. finish honing. Defined.
imports: Tutorial