Did you consider using dependent types to define the image database in such a way that it's impossible to create one that's not InternallyConsistent? This approach can often make proofs shorter/simpler.