right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q = p ∨ q ∈ U
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q ∈ U