def internal_head_le_mem_step

bend-mathlib@0.8.1.0 · list.bend:993

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

993def internal_head_le_mem_step(+x: Nat, +z: Nat, -t: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(z, y) == b : Bool}, hxz: MNat.le(x, z), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, t, y)) == True{} : Bool}, ih: {List.contains(~Nat, ~Nat.is_eq, t, y) == True{} : Bool} -> MNat.le(z, y)) -> MNat.le(x, y):
994  match b:
995    case True{}:
996      %MNat.eq_of_is_eq(z, y, e) : MNat.le(x, _)
997      hxz
998    case False{}:
999      MNat.le_trans(x, z, y, hxz, ih(hm))