proposition: Theorem SharpenedGuard : FullySharpened GuardSpec.
proof: Proof. guardc. Defined.
imports: Fiat.ADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTablesGuard