proposition: Lemma RunsTo_Equal_left_fast : forall {av st1 st2}, M.Equal st1 st2 -> forall env prog st', @RunsTo av env prog st1 st' -> @RunsTo av env prog st2 st'.
proof: Proof. intros * eq **; rewrite <- eq; assumption. Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program