simp only [LogicalConnective.HomClass.map_or, LogicalConnective.Prop.or_eq]
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬((Evalf (Model.structure T Γ) Semiterm.fvar) p ∨ (Evalf (Model.structure T Γ) Semiterm.fvar) q)