fact: Definition guard_init (_: unit) : ComputationalADT.cRep GuardImpl := simp (CallConstructor GuardImpl "Init").
imports: Narcissus.Examples.Guard.StatefulGuard Fiat.QueryStructure.Automation.MasterPlan Narcissus.Examples.Guard.Core Narcissus.OCamlExtraction.Extraction