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

import Base
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

def fa_app(+seq: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(seq, G.AaGCuts.append(xs, ys)) == Bool.or(G.AaGSeq.fits_any(seq, xs), G.AaGSeq.fits_any(seq, ys)) : Bool}:
  match xs:
    case Nil{}:
      {==}
    case Con{d, t}:
      %Equal.sym(Bool, G.AaGSeq.fits_any(seq, G.AaGCuts.append(t, ys)), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)), fa_app(seq, t, ys)) : {Bool.or(G.AaGSeq.fits(seq, d), _) == Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)) : Bool}
      Equal.sym(Bool, Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)), Bool.or(G.AaGSeq.fits(seq, d), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys))), b.or_assoc(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok