proposition: Lemma class_of_union_1: forall `{WF} x y z, {{t}} x z \/ {{t}} y z -> NumSet.Equal (class_of (union t x y) z) (NumSet.union (class_of t x) (class_of t y)).
proof: Proof. intros t Hwf x y z [H|H]; symmetry in H. setoid_replace (class_of (union t x y) z) with (class_of (union t x y) x) by (apply class_of_compat; rewrite sameclass_union; auto). apply class_of_union; trivial. setoid_replace (class_of (union t x y) z) with (class_of (union t x y) y) by (apply class_of_compat; rewrite sameclass_union; auto). rewrite <- class_of_union by trivial. apply class_of_compat. symmetry. rewrite sameclass_union by trivial. right. left. split; reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)