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

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_join(+ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(ys, acc) == V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())) : V.AaAcc}:
  match ys:
    case Nil{}:
      Equal.sym(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.empty()), acc, acc.join_empty_r(acc))
    case Con{g, t}:
      Equal.trans(V.AaAcc, V.AaAcc.from(t, V.AaAcc.join(acc, V.AaAcc.single(g))), V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), from_join(t, V.AaAcc.join(acc, V.AaAcc.single(g))), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), acc.join_assoc(acc, V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty())), Equal.sym(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), Equal.trans(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.single(g), V.AaAcc.from(t, V.AaAcc.empty()))), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, x), V.AaAcc.from(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g))), V.AaAcc.join(V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.from(t, V.AaAcc.empty())), from_join(t, V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)))), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, V.AaAcc.join(x, V.AaAcc.from(t, V.AaAcc.empty()))), V.AaAcc.join(V.AaAcc.empty(), V.AaAcc.single(g)), V.AaAcc.single(g), acc.join_empty_l(V.AaAcc.single(g)))))))

Uses (13):
  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_empty_l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=acc.join_empty_r
  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/eval.bend&name=AaAcc.single
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaGrant