Theorem: Term.pos_var (WTA.lean)

State before:
Δ : RankedAlphabet
H : Type
v : H
⊢ Vars Δ H (var v)
Tactic:
simp [Vars]
State after:
no goals