rintro ⟨hp, hq⟩
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1
case mpr.intro
α : 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
hq : q ∈ t.tableau.1
⊢ p ⋏ q ∈ t.tableau.1