ext j
case mp
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
⊢ trunc w = w
case mp.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
j : Fin (Nat.succ n)
⊢ trunc w j = w j