|- (∀x. MEM x [] ⇔ F) ∧ ∀x h t. MEM x (h::t) ⇔ (x = h) ∨ MEM x t |- (match [] [] v0 ⇔ T) ∧ (match [] (v8::v9) v2 ⇔ F) ∧ (match (Epsilon::t) w s ⇔ match t w s) ∧ (match (Charset C::t) [] s ⇔ F) ∧ (match (Charset C::t) (d::w) s ⇔ MEM d C ∧ match t w NONE) ∧ (match (r1 + r2::t) w s ⇔ match (r1::t) w s ∨ match (r2::t) w s) ∧ (match (r1 # r2::t) w s ⇔ match (r1::r2::t) w s) ∧ (match (Repeat r::t) w s ⇔ if s = SOME (Repeat r::t) then F else match t w s ∨ match (r::Repeat r::t) w (SOME (Repeat r::t)))