proposition: Lemma lem_big_step_deterministic : forall c s s1, c >> s ==> s1 -> forall s2, c >> s ==> s2 -> s1 = s2.
proof: Proof. induction 1; sauto brefl: on. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String