def aes_nat_tail_ne

qasim-bend-kit@0.1.0.2 · PROOF.bend:372

import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF

import Base

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

Uses (3)

Used by (1)

qasim-bend-kit@0.1.0.2/PROOF:aes_nat_eq_none_if_ne