Theorem: starAntitone (Fine/SystemB/Theories.lean)

State before:
⊢ Antitone primeStarFunction
Tactic:
intros _ _ h₁ f h₂ h₃
State after:
a✝ b✝ : Pr
h₁ : a✝ ≤ b✝
f : Form
h₂ : f ∈ (fun a => ↑a) ((fun a => ↑a) (primeStarFunction b✝))
h₃ : ~f ∈ ↑↑a✝
⊢ False

State before:
a✝ b✝ : Pr
h₁ : a✝ ≤ b✝
f : Form
h₂ : f ∈ (fun a => ↑a) ((fun a => ↑a) (primeStarFunction b✝))
h₃ : ~f ∈ ↑↑a✝
⊢ False
Tactic:
exact h₂ (h₁ h₃)
State after:
no goals