def b_cg_con

bendtorch@1.3.0.0 · PROOF.bend:630

import Base
import bendtorch@1.3.0.0/main.bend as T

630def b_cg_con(-m: Nat, -x: T.BG, -t: List<&1, T.BG>, -acc: List<&1, T.BG>, r: b_CGR<m, t, x <> acc>) -> b_CGR<1n+m, x <> t, acc>:
631  match r:
632    case b_CGR{hh, same, cat}:
633      b_CGR{hh, same, cat}