intro ys a3
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
⊢ ∀ (a : List α), (s.is_nullable ∧ a = []) ∧ xs ++ a = cs → (r.is_nullable ∧ s.is_nullable) ∧ cs = []
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3 : (s.is_nullable ∧ ys = []) ∧ xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []