def h.low

bend-kit-collections@0.1.4.1 · PROOF.bend:1891

import Base

1891def h.low(a: Bool, t: Cmp, e: {Cmp.is_eq(Word.cmp.fin(Bool.and(a, False{}), False{}, t)) == False{} : Bool})
1892  -> {Cmp.is_eq(t) == False{} : Bool}:
1893  match a:
1894    case True{}:
1895      match t:
1896        case LT{}:
1897          e
1898        case EQ{}:
1899          e
1900        case GT{}:
1901          e
1902    case False{}:
1903      match t:
1904        case LT{}:
1905          e
1906        case EQ{}:
1907          e
1908        case GT{}:
1909          e