proposition: Lemma RemoveSkips_RunsTo_iff {av} : forall prog pre post env, @RunsTo av env (RemoveSkips prog) pre post <-> @RunsTo av env prog pre post.
proof: Proof. intuition eauto using RemoveSkips_RunsTo, RemoveSkips_RunsTo2. Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program