def un.band_t

bend-osdev-u32@0.1.0.0 · PROOF.bend:1908

import Base

1908def un.band_t(x: Bool) -> {Bool.and(x, True{}) == x : Bool}:
1909  match x:
1910    case True{}:
1911      {==}
1912    case False{}:
1913      {==}