[STATEMENT]
lemma ACI_set_eq:
  fixes r s :: "'a rexp"
  assumes "r ~ s"
  shows "set_rexp r = set_rexp s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_rexp r = set_rexp s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r ~ s

goal (1 subgoal):
 1. set_rexp r = set_rexp s
[PROOF STEP]
by (induct r s rule: ACI.induct) auto