proposition: Lemma statesetset_map_cardinal: StateSetSet.cardinal (statesetset_map f t0) = StateSetSet.cardinal t0.
proof: Proof. refine (proj2 (StateSetSetProps.Props.fold_rec_bis (P:=fun t a => (forall p, StateSetSet.In p t0 -> (StateSetSet.In (f p) a <-> StateSetSet.In p t)) /\ ((forall p, StateSetSet.In p t -> StateSetSet.In p t0) -> StateSetSet.cardinal a = StateSetSet.cardinal t)) _ _ _) _); trivial. intros. setoid_rewrite <- H. trivial. split; trivial. StateSetSetProps.setdec. intros p a t' Hp Hp' [IH IHc]. split. intros q Hq. StateSetSetProps.Facts.set_iff. specialize (IH q Hq). rewrite Hf by auto. tauto. intros Ht'. rewrite (StateSetSetProps.Props.cardinal_2 (s:=a) (x:=f p)); auto with set. symmetry. rewrite (StateSetSetProps.Props.cardinal_2 (s:=t') (x:=p)); auto with set. symmetry. rewrite IHc; auto. intros q Hq. apply Ht'. StateSetSetProps.setdec. rewrite IH; auto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)