exact ⟨exp (v 0), by simp [h.le], rfl, h⟩
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ∈ v 1
⊢ ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
no goals