proposition: Theorem plus2_spec : forall st n st', st X = n -> st =[ plus2 ]=> 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(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)