Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.iff_cons (Logic/Modal/Standard/Geach.lean)

State before:
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
l : List Axioms.Geach.Taple
⊢ 𝗚𝗲(x :: l) = 𝗴𝗲(x) ∪ 𝗚𝗲(l)
Tactic:
simp only [MultiGeach]
State after:
no goals