proposition: Lemma RemoveSkip_left_Safe: forall (av : Type) (env : Env av) (st : State av) (a b : Stmt), RemoveSkips a = Skip -> Safe env (Seq a b) st -> Safe env b st.
proof: Proof. intros av env st a b eq safe. induction a; simpl in *; try facade_inversion; destruct_conjs; try discriminate. - eauto with runsto_safe. - destruct_Is_Skip a1. { apply H0; econstructor; apply RemoveSkips_RunsTo; rewrite ?eq, ?eq0; constructor; reflexivity. } { destruct_Is_Skip a2; (discriminate || intuition). } Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program