proposition: Theorem ceval_deterministic' : forall c st st1 st2, st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2.
proof: Proof. intros c st st1 st2 He1 He2. apply ceval__ceval_step in He1. apply ceval__ceval_step in He2. inversion He1 as [i1 E1]. inversion He2 as [i2 E2]. apply ceval_step_more with (i2 := i1 + i2) in E1. apply ceval_step_more with (i2 := i1 + i2) in E2. rewrite E1 in E2. inversion E2. reflexivity. lia. lia. Qed.
imports: Coq(Lia) Coq(Arith.Arith) Coq(Arith.PeanoNat) Coq(Arith.EqNat) LF(Imp Maps)