L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0) ↔ NoTopOrder M
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noTopOrderSentence Language.order ↔ NoTopOrder M
simp only [noTopOrderSentence, 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
⊢ NoTopOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0) ↔ NoTopOrder M
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoTopOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoTopOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
intro h a
no goals
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoTopOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
exact exists_not_le a