proposition: Theorem ceval_deterministic: forall c st st1 st2, st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2.
proof: Proof. intros c st st1 st2 E1 E2. generalize dependent st2; induction E1; intros st2 E2; inversion E2; subst; try find_rwd; try find_eqn; auto. - + find_rwd. - + find_rwd. Qed.
imports: Coq(Lia) LF(Maps) LF(Imp)