apply Nonempty.intro
Γ : Type
inst✝ : Alphabet Γ
⊢ Nonempty (Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty))
case val
Γ : Type
inst✝ : Alphabet Γ
⊢ Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty)