~/jendhub

def lt_succ.lift

minebender-game@1.0.0.0 · proof_base.bend:189

import minebender-game@1.0.0.0/proof_base.bend as ProofBase
import Base

189def lt_succ.lift(+j: Nat, +q: Nat,
190  r: Or({Nat.is_lt(j, q) == True{} : Bool}, {j == q : Nat})) ->
191  Or({Nat.is_lt(1n+j, 1n+q) == True{} : Bool}, {1n+j == 1n+q : Nat}):
192  match r:
193    case Inl{lt}:
194      Inl{lt}
195    case Inr{eq}:
196      %eq : Or({Nat.is_lt(1n+j, 1n+q) == True{} : Bool}, {1n+j == 1n+_ : Nat})
197      Inr{{==}}

Uses (5)

Used by (1)