Theorem: freshVarProg_is_fresh (Pdl/Fresh.lean)

State before:
α : Program
⊢ freshVarProg α ∉ voc α
Tactic:
have := freshVarProg_is_larger α
State after:
α : Program
this : ∀ n ∈ voc α, n < freshVarProg α
⊢ freshVarProg α ∉ voc α

State before:
α : Program
this : ∀ n ∈ voc α, n < freshVarProg α
⊢ freshVarProg α ∉ voc α
Tactic:
simp [freshVarProg, voc, vocabOfFormula] at *
State after:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α

State before:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α
Tactic:
by_contra hyp
State after:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False

State before:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False
Tactic:
specialize this (freshVarProg α)
State after:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False

State before:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False
Tactic:
have := Nat.lt_irrefl (freshVarProg α)
State after:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this✝ : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
this : ¬freshVarProg α < freshVarProg α
⊢ False

State before:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this✝ : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
this : ¬freshVarProg α < freshVarProg α
⊢ False
Tactic:
tauto
State after:
no goals