PROOF.sig.mgo: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3630-3635 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=3630&end_line=3635

import Base
import bend-osdev-apparmor@0.1.0.0/rule_signal.bend as RS

def sig.mgo(+hit: Bool, +r: RS.AaSignalRule, +a: List<&2, RS.AaSignalRule>, +b: List<&2, RS.AaSignalRule>) -> {RS.AaSignalRule.matching.go(hit, r, RS.AaSignalRule.append(a, b)) == RS.AaSignalRule.append(RS.AaSignalRule.matching.go(hit, r, a), b) : List<&2, RS.AaSignalRule>}:
  match hit:
    case True{}:
      {==}
    case False{}:
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_signal.bend&name=AaSignalRule
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_signal.bend&name=AaSignalRule.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_signal.bend&name=AaSignalRule.matching.go