proposition: Lemma fold_pair {A B A' B' V} : forall (m : t V) (ab : A * B) (f : TKey -> V -> (A' * B')) fa fb, @fold V (A * B) (fun k (v : V) (ab : A * B) => let (a, b) := f k v in let (a', b') := ab in (fa k a a', fb k b b')) m ab = (fold (fun k m (a' : A) => fa k (fst (f k m)) a') m (fst ab), fold (fun k m (b' : B) => fb k (snd (f k m)) b') m (snd ab)).
proof: Proof. intros; repeat rewrite fold_1; revert ab; induction (elements m); destruct ab; simpl; eauto. destruct a; simpl; destruct (f k v); rewrite IHl; reflexivity. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances