type b_MARF

bendtorch@1.3.0.0 · PROOF.bend:738

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

738type b_MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type:
739  b_MARF{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {b_ffmap(h, dm, List.append(&1, T.BG, a, b)) == List.append(&1, T.DB, b_ffmap(h, dm, a), b_ffmap(h, dm, b)) : List<&1, T.DB>}}