def fe_app

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:99

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

99def fe_app(+r: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.append(xs, ys)) == Bool.or(fe_any(r, xs), fe_any(r, ys)) : Bool}:
100  match xs:
101    case Nil{}:
102      {==}
103    case Con{d, t}:
104      %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(t, ys)), Bool.or(fe_any(r, t), fe_any(r, ys)), fe_app(r, t, ys)) : {Bool.or(fe(r, d), _) == Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)) : Bool}
105      Equal.sym(Bool, Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)), Bool.or(fe(r, d), Bool.or(fe_any(r, t), fe_any(r, ys))), b.or_assoc(fe(r, d), fe_any(r, t), fe_any(r, ys)))