Theorem: LO.Modal.Standard.DeductionParameter.Geach.subset_axm (Logic/Modal/Standard/Geach.lean)

State before:
α : Type u_1
Ax : AxiomSet α
l₁ l₂ : List Axioms.Geach.Taple
h : autoParam (l₁ ⊆ l₂) _auto✝
⊢ Ax(𝐆𝐞(l₁)) ⊆ Ax(𝐆𝐞(l₂))
Tactic:
simp_all
State after:
no goals