fact: Example ceval_example1: (X ::= ANum 2;; IFB BLe (AId X) (ANum 1) THEN Y ::= ANum 3 ELSE Z ::= ANum 4 FI) / empty_state \\ (t_update (t_update empty_state X 2) Z 4).
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps