def equal_of_is_eq

stelliferous@0.0.2.0 · proofs/nat_order.bend:21

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

21def equal_of_is_eq(+left: Nat,+right: Nat,equal: {Nat.is_eq(left,right) == True{} : Bool}) -> {left == right : Nat}:
22  match left right:
23    case 0n 0n: {==}
24    case 0n 1n+rest: Empty.absurd({0n == 1n+rest : Nat},WordEncoding.false_true(equal))
25    case 1n+rest 0n: Empty.absurd({1n+rest == 0n : Nat},WordEncoding.false_true(equal))
26    case 1n+ +previous 1n+ +last:
27      %equal_of_is_eq(previous,last,equal) : {1n+previous == 1n+_ : Nat}
28      {==}