segment-tree

inductive W (A : Type) (B : A → Type) where
  | mk (a : A) (f : B a → W A B) : W A B

def wInd {A : Type} {B : A → Type} {p : W A B → Type}
  (step : (a : A) → (f : B a → W A B) → (∀ (b : B a), p (f b)) → p (W.mk a f))
    (t : W A B) : p t :=
  match t with
  | W.mk a f => step a f (fun b => wInd step (f b))

-- N

segment-tree

-- ==========================================
-- 1. 基础架构：W-类型 (MLTT 核心)
-- ==========================================

inductive W (A : Type) (B : A → Type) where
  | mk (a : A) (f : B a → W A B) : W A B

def wInd {A : Type} {B : A → Type} {p : W A B → Type}
  (step : (a : A) → (f : B a → W A B) → (∀ (b : B a), p (f b)) → p (W.mk a f))
    (t : W A B) : p t :=