. exact conj₁'! h;
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p

case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a