proposition: Theorem plus2_spec : forall st n st', st X = n -> plus2 / st \\ st' -> st' X = n + 2.
proof: Proof. intros st n st' HX Heval. inversion Heval. subst. clear Heval. simpl. apply t_update_eq. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps