Add in_domain, rev_assoc, merge and union
Introduce definition in_domain_prop
Proper implicit arguments for added definitions
Add fold
Theorems relating in_domain to in_domain_prop
Add proof of invariant for merge