proposition: Lemma RemoveSkips_RunsTo {av} : forall prog pre post env, @RunsTo av env (RemoveSkips prog) pre post -> @RunsTo av env prog pre post.
proof: Proof. induction prog; RemoveSkips_helper. + destruct_Is_Skip prog1; destruct_Is_Skip prog2; RemoveSkips_helper. + remember (While e RemoveSkips prog)%facade eqn:Heq. induction H; try congruence; unfold loop in *; inversion Heq; subst; clear Heq; RemoveSkips_helper. Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program