def b_l1
import bendtorch@1.3.0.0/PROOF.bend as PROOFimport Base
import bendtorch@1.3.0.0/main.bend as T
577def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R<h, dm, xs, acc>:
578 match xs:
579 case Nil{}:
580 b_L1R{Nil{}, {==}, {==}}
581 case Con{x, t}:
582 b_l1_con(x, t, h, dm, acc, b_l1(t, h, dm, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc))