L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1) ↔ NoBotOrder M
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noBotOrderSentence Language.order ↔ NoBotOrder M
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
  BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize, Term.realize_le,
  Sum.elim_inr]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoBotOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1) ↔ NoBotOrder M
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoBotOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoBotOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
intro h a
no goals
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoBotOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
exact exists_not_ge a