[STATEMENT]
lemma horn_infer1_union:
  "horn.infer1 (\<H>\<^sub>1 \<union> \<H>\<^sub>2) x B = horn.infer1 \<H>\<^sub>1 x B \<union> horn.infer1 \<H>\<^sub>2 x B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horn.infer1 (\<H>\<^sub>1 \<union> \<H>\<^sub>2) x B = horn.infer1 \<H>\<^sub>1 x B \<union> horn.infer1 \<H>\<^sub>2 x B
[PROOF STEP]
by (auto simp: horn.infer1_def)