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

State before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗚𝗲([]) = 𝗞
Tactic:
simp [MultiGeach]
State after:
no goals