[STATEMENT]
lemma match_sound:
  assumes "match t p = Some \<sigma>"
  shows "\<sigma> \<in> matchers {(p, t)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<in> matchers {(p, t)}
[PROOF STEP]
using match_list_sound [of Var "[(p, t)]"] and assms
[PROOF STATE]
proof (prove)
using this:
match_list Var [(p, t)] = Some ?\<sigma> \<Longrightarrow> ?\<sigma> \<in> matchers (set [(p, t)])
match t p = Some \<sigma>

goal (1 subgoal):
 1. \<sigma> \<in> matchers {(p, t)}
[PROOF STEP]
by (simp add: match_def)