proposition: Lemma fold_init : forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').
proof: Proof. intros. apply fold_rel with (R:=eqA); auto. intros. apply Comp; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface