constructor <;> [rintro ⟨rfl, rfl⟩; rintro rfl] <;> [rfl; constructor <;> rfl]
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a✝ b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
a : List σ
x✝ : c ∈ a
⊢ b = head✝.start_state ∧ a = head✝.stop_state_list ↔ { start_state := b, stop_state_list := a } = head✝
no goals