proposition: Lemma match_config_skip: forall C k s pc, compile_cont C k pc -> match_config C (SKIP, k, s) (pc, nil, s).
proof: Proof. intros. constructor. - cbn. inversion H; eauto with code. - cbn. autorewrite with code. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)