proposition: Theorem ceval_deterministic'_alt: forall c st st1 st2, st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2.
proof: Proof. Proof with auto. intros c st st1 st2 E1 E2; generalize dependent st2; induction E1; intros st2 E2; inversion E2; subst... - rewrite (IHE1_1 st'0 H1) in *... - + rewrite H in H5. discriminate. - + rewrite H in H5. discriminate. - + rewrite H in H2. discriminate. - rewrite H in H4. discriminate. - rewrite (IHE1_1 st'0 H3) in *... Qed.
imports: Coq(Lia) LF(Maps) LF(Imp)