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