exists σ⬝a
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ ∃ a, treeₑ a = app (some σ) w
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
⊢ treeₑ (σ⬝a) = app (some σ) w