Theorem: NoVars.fromNat (SInfinity/Basic.lean)

State before:
n : ℕ
⊢ NoVars (Sinf_term.fromNat n)
Tactic:
induction n <;> try constructor <;> assumption
State after:
no goals

State before:
case succ
n✝ : ℕ
n_ih✝ : NoVars (Sinf_term.fromNat n✝)
⊢ NoVars (Sinf_term.fromNat (Nat.succ n✝))
Tactic:
constructor <;> assumption
State after:
no goals