proposition: Lemma cardinal_domain t: StateSetSet.cardinal (domain t) = StateSetMap.cardinal t.
proof: Proof. refine (proj2 (StateSetMapProps.fold_rec_bis (P:=fun t a => (forall p, StateSetSet.In p a <-> StateSetMap.In p t) /\ StateSetSet.cardinal a = StateSetMap.cardinal t) _ _ _)). intros. setoid_rewrite <- H. trivial. split; trivial. split. StateSetSetProps.setdec. StateSetMapProps.map_iff. tauto. intros p np a t' Hp Hp' [IH IHc]. split. intro q. StateSetSetProps.set_iff. StateSetMapProps.map_iff. specialize (IH q). tauto. rewrite (StateSetMapProps.cardinal_2 Hp') by (intro; reflexivity). rewrite (StateSetSetProps.Props.cardinal_2 (s:=a) (x:=p)). congruence. rewrite IH; trivial. auto with set. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)