proposition: Lemma fold_rel : forall (A B:Type)(R : A -> B -> Type) (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B) (m : t elt), R i j -> (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) -> R (fold f m i) (fold g m j).
proof: Proof. intros A B R f g i j m Rempty Rstep. rewrite 2 fold_spec_right. set (l:=rev (elements m)). assert (Rstep' : forall k e a b, InA eqke (k,e) l -> R a b -> R (f k e a) (g k e b)) by (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; assumption). clearbody l; clear Rstep m. induction l; simpl; auto. apply Rstep'; auto. destruct a; simpl; rewrite InA_cons; left; red; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface