proposition: Lemma rep_inv_ptr : forall p a, rep_inv p a ===> p =?> 1 * any.
proof: Proof. destruct a; unfold rep_inv, Monitors_rep_inv; simpl; sepLemma; apply any_easy. Qed.
imports: Coq.Lists.List Coq.Program.Program Coq.Arith.Arith Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Fiat4Monitors.RADL_Topics Fiat.Fiat4Monitors.RADL_Messages Fiat.Fiat4Monitors.RADL_Flags Fiat.Fiat4Monitors.RADL_Nodes Fiat.Fiat4Monitors.MonitorADTs Bedrock.Platform.Facade.DFacade Bedrock.Platform.Facade.Notations Bedrock.Platform.Cito.ADT Bedrock.Platform.Cito.RepInv