proposition: Lemma RunsTo_Equal_right_fast : forall {av st1 st2}, M.Equal st1 st2 -> forall env prog st', @RunsTo av env prog st' st1 -> @RunsTo av env prog st' st2.
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