def passes_add

bendtorch@1.3.0.0 · PROOF.bend:1058

import Base
import bendtorch@1.3.0.0/spec.bend as Spec

1058# r + p passes are p passes, then r more
1059def passes_add(r: Nat, +p: Nat, +xs: List<&2, Spec.Sum>) -> {Spec.passes(Nat.add(r, p), xs) == Spec.passes(r, Spec.passes(p, xs)) : List<&2, Spec.Sum>}:
1060  match r:
1061    case 0n:
1062      {==}
1063    case 1n+q:
1064      # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run
1065      Equal.cong(List<&2, Spec.Sum>, List<&2, Spec.Sum>, z => Spec.spass(z), Spec.passes(Nat.add(q, p), xs), Spec.passes(q, Spec.passes(p, xs)), passes_add(q, p, xs))