proposition: Lemma decode_encode_mach_input_rw: forall M w, decode_mach_input (encode_mach_input M w) = (M, w).
proof: Proof. intros. unfold decode_mach_input. unfold encode_mach_input. rewrite decode_encode_pair_rw. rewrite decode_encode_mach_rw. reflexivity. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop