def fin_of_none
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:21
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
21def fin_of_none(+bound: Nat, +value: Nat, misses: {False{} == Nat.is_lt(value, bound) : Bool}) -> {None{} == Laws.fin_of(bound, value) : Maybe<&2, Shape.Fin(bound)>}:
22 match bound value:
23 case 0n value:
24 {==}
25 case 1n+p 0n:
26 Empty.absurd({None{} == Laws.fin_of(1n+p, 0n) : Maybe<&2, Shape.Fin(1n+p)>}, Nats.contradiction(Nat.is_lt(0n, 1n+p), {==}, misses))
27 case 1n+p 1n+q:
28 Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), None{}, Laws.fin_of(p, q), fin_of_none(p, q, misses))