def no_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/api.bend:267

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

267def no_len(-G: Type, +n: Nat, +m: Nat, +h: {n == m : Nat}, +hf: {Nat.is_eq(n, m) == False{} : Bool}) -> G:
268  Empty.absurd(G, L.false_true(Equal.trans(Bool, False{}, Nat.is_eq(n, m), True{}, Equal.sym(Bool, Nat.is_eq(n, m), False{}, hf),
269    Equal.trans(Bool, Nat.is_eq(n, m), Nat.is_eq(m, m), True{}, Equal.cong(Nat, Bool, x => Nat.is_eq(x, m), n, m, h), N.is_eq_refl(m)))))