proposition: Theorem ceval_deterministic'_alt: forall c st st1 st2, c / st \\ st1 -> c / st \\ st2 -> st1 = st2.
proof: Proof. Proof with auto. intros c st st1 st2 E1 E2; generalize dependent st2; induction E1; intros st2 E2; inv E2... - assert (st' = st'0) as EQ1... subst st'0... - + rewrite H in H5. inversion H5. - + rewrite H in H5. inversion H5. - + rewrite H in H2. inversion H2. - rewrite H in H4. inversion H4. - assert (st' = st'0) as EQ1... subst st'0... Qed.
imports: Coq.omega.Omega Maps Imp