fact: Definition guard_process_packet (bs: bytes) (rep: ComputationalADT.cRep GuardImpl) : (_ * result) := simp (CallMethod GuardImpl "ProcessPacket" rep bs).
imports: Narcissus.Examples.Guard.Guard Narcissus.OCamlExtraction.Extraction