[STATEMENT]
lemma normalized_dst_ips_def2: "normalized_dst_ips ms = normalized_n_primitive (is_Dst, dst_sel) normalized_cidr_ip ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_dst_ips ms = normalized_n_primitive (is_Dst, dst_sel) normalized_cidr_ip ms
[PROOF STEP]
by(induction ms rule: normalized_dst_ips.induct, simp_all add: normalized_cidr_ip_def)