Is Regular inf

@[simp]theorem IsRegular.inf {p1 p2 : ωLanguage Symbol}    (h1 : p1.IsRegular) (h2 : p2.IsRegular) : (p1 ⊓ p2).IsRegular := by  obtain ⟨State1, h_fin1, ⟨na1, acc1⟩, rfl⟩ := h1  obtain ⟨State2, h_fin1, ⟨na2, acc2⟩, rfl⟩ := h2  let State : Bool → Type    | false => State1 | true => State2  let na : (i : Bool) → NA (State i) Symbol    | false => na1 | true => na2  let acc : (i : Bool) → Set (State i)    | false => acc1 | true => acc2  have : ∀ i, Finite (State i) := by grind  use (Π i : Bool, State i) × Bool, inferInstance, ⟨(interNA na acc), interAccept acc⟩  apply mem_ext  intro xs  simp only [inter_language_eq, mem_inf, mem_language]  rw [mem_iInf, Bool.forall_bool]  rfl