simp [List.conj'_cons_nonempty h]
case hcons
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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : ∀ g ∈ r :: Γ, g = p
⊢ 𝓢 ⊢! p ⟶ (r :: Γ).conj'
case hcons
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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : ∀ g ∈ r :: Γ, g = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'