proposition: Lemma is_false_Equal_fast : forall {av st1 st2}, M.Equal st1 st2 -> forall e, @is_false av st1 e -> @is_false av st2 e.
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