def somes_nones

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:225

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

225def somes_nones(+count: Nat) -> {Laws.somes(Backward.nones(count)) == Laws.falses(count) : List<&2, Bool>}:
226  match count:
227    case 0n:
228      {==}
229    case 1n+rest:
230      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs, Laws.somes(Backward.nones(rest)), Laws.falses(rest), somes_nones(rest))