def internal_and_true_sym

bend-mathlib@0.8.1.0 · nat.bend:2449

import Base

2449def internal_and_true_sym(x: Bool) -> {x == Bool.and(x, True{}) : Bool}:
2450  match x:
2451    case False{}:
2452      {==}
2453    case True{}:
2454      {==}