def lift_upper_bound

stelliferous@0.0.2.0 · proofs/nat_order.bend:86

import Base

86def lift_upper_bound(+value: Nat,+limit: Nat,bound: UpperBound<value,limit>) -> UpperBound<1n+value,1n+limit>:
87  match bound:
88    case Before{inside}: Before{inside}
89    case At{equal}: At{Equal.cong(Nat,Nat,n => 1n+n,value,limit,equal)}