Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁ (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ q ∈ t.tableau.1
Tactic:
exact t.not_mem₂_iff_mem₁.mp $ not_mem₂ (by simpa) (show 𝓓 ⊢! List.conj' [p] ⟶ q by simpa;)
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.tableau.1
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ 𝓓 ⊢! [p].conj' ⟶ q
Tactic:
simpa
State after:
no goals