proposition: Theorem ceval__ceval_step: forall c st st', st =[ c ]=> st' -> exists i, ceval_step st c i = Some st'.
proof: Proof. intros c st st' Hce. induction Hce. Admitted. Theorem ceval_and_ceval_step_coincide: forall c st st', st =[ c ]=> st' <-> exists i, ceval_step st c i = Some st'. Proof. intros c st st'. split. apply ceval__ceval_step. apply ceval_step__ceval. Qed.
imports: Coq(Lia) Coq(Arith.Arith) Coq(Arith.PeanoNat) Coq(Arith.EqNat) LF(Imp Maps)