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; auto. - rewrite (IHE1_1 st'0 H1) in *. auto. - + rewrite (IHE1_1 st'0 H3) in *. auto. Qed.
imports: Coq(Lia) LF(Maps) LF(Imp)