PROOF.inc.acc: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3493-3494 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=3493&end_line=3494

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

def inc.acc(+g0: List<&2, P.AaGrant>, +g1: List<&2, P.AaGrant>) -> {V.AaAcc.of(P.AaGrant.append(P.AaGrant.append(g0, g1), g1)) == V.AaAcc.of(P.AaGrant.append(g0, g1)) : V.AaAcc}:
  Equal.trans(V.AaAcc, V.AaAcc.from(P.AaGrant.append(P.AaGrant.append(g0, g1), g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_app(P.AaGrant.append(g0, g1), g1, V.AaAcc.empty()), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.from(g1, x), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_idem(g1, V.AaAcc.from(g0, V.AaAcc.empty())), Equal.sym(V.AaAcc, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())))))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=from_app
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=from_idem
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc.empty
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc.from
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaAcc.of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaGrant
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaGrant.append