Theorem: Term.ε_mem_pos (WTA.lean)

State before:
Δ : RankedAlphabet
H : Type
ξ : (Term.algebra Δ H).carrier
⊢ Word.ε ∈ Hom.hom pos ξ
Tactic:
sorry
State after:
no goals