def internal_and_right

bend-mathlib@0.8.1.0 · list.bend:732

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

732def internal_and_right(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
733  match a:
734    case False{}:
735      Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(h))
736    case True{}:
737      h