induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! verum!;
| hsingle => simp_all; exact generalConj'! h;
| hcons p Γ hne ih => simp_all; exact implyRightAnd! (generalConj'! h.1) ih;
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 𝓢
h : ∀ p ∈ Γ, p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
no goals