PROOF.pm.assoc: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3241-3248 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=3241&end_line=3248

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P

def pm.assoc(+a: P.AaPerms, +b: P.AaPerms, +c: P.AaPerms) -> {P.AaPerms.union(P.AaPerms.union(a, b), c) == P.AaPerms.union(a, P.AaPerms.union(b, c)) : P.AaPerms}:
  match a:
    case P.AaPerms{x}:
      match b:
        case P.AaPerms{y}:
          match c:
            case P.AaPerms{z}:
              Equal.cong(List<&2, Bool>, P.AaPerms, l => P.AaPerms{l}, P.AaBits.or(P.AaBits.or(x, y), z), P.AaBits.or(x, P.AaBits.or(y, z)), bits.or_assoc(x, y, z))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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/PROOF.bend&name=bits.or_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.or
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.union