def natural_clash
bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:220
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
220def natural_clash(+left: Nat, +right: Nat, equal: {left == right : Nat},
221 different: {Nat.is_eq(left, right) == False{} : Bool}) -> Empty:
222 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(left, right), False{},
223 Equal.sym(Bool, Nat.is_eq(left, right), True{},
224 %equal : {Nat.is_eq(left, _) == True{} : Bool}
225 nat_equal_self(left)), different))