PROOF.aes_nat_tail_ne: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
Lines 372-374 of qasim-bend-kit@0.1.0.2/PROOF.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&start_line=372&end_line=374

import Base

def aes_nat_tail_ne(+a: Nat, +b: Nat,
    no: {1n+a != 1n+b : Nat}) -> {a != b : Nat}:
    e => no(Equal.cong(Nat, Nat, n => 1n+n, a, b, e))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat