proposition: Lemma all1_ok : moduleOk all1.
proof: Proof. link m1_ok m2_ok. Qed.
imports: Coq.Strings.String Coq.Bool.Bool 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.RADLNodeADTs Fiat.Fiat4Monitors.LandsharkTopics Fiat.Fiat4Monitors.LandsharkNodes Bedrock.Platform.Facade.DFacade Bedrock.Platform.Facade.Notations Bedrock.Platform.Cito.ADT Bedrock.Platform.Cito.RepInv Bedrock.Platform.AutoSep Bedrock.Platform.Facade.CompileUnit2 Bedrock.Platform.Facade.CompileDFModule Bedrock.Platform.Facade.DFacadeToBedrock2