proposition: Lemma RemoveSkips_RunsTo2 {av} : forall prog pre post env, @RunsTo av env prog pre post -> @RunsTo av env (RemoveSkips prog) pre post.
proof: Proof. induction prog; RemoveSkips_helper. + destruct_Is_Skip prog1; destruct_Is_Skip prog2; try solve [RemoveSkips_helper]; specialize (IHprog1 _ _ _ H2); specialize (IHprog2 _ _ _ H5); repeat facade_inversion; try match goal with | [ H: M.Equal _ _ |- _ ] => rewrite H in * end; eauto using Equal_trans with runsto_safe. + dependent induction H; eauto with runsto_safe. Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program