PROOF.from_idem: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3483-3484 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=3483&end_line=3484

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 from_idem(+ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(ys, V.AaAcc.from(ys, acc)) == V.AaAcc.from(ys, acc) : V.AaAcc}:
  Equal.trans(V.AaAcc, V.AaAcc.from(ys, V.AaAcc.from(ys, acc)), V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), from_join(ys, V.AaAcc.from(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(x, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.from(ys, acc), acc.join_assoc(acc, V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, x), V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty()), acc.join_idem(V.AaAcc.from(ys, V.AaAcc.empty()))), Equal.sym(V.AaAcc, V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc))))))

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=acc.join_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=acc.join_idem
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=from_join
  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.join
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaGrant