proposition: Lemma values_are_done : forall D t, isVal t = true -> machine_step D (initconf t) = Done _.
proof: Proof. intros D t VV. destruct t; simpl in *; try discriminate. auto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen