Add project work on iTrees (monads, exists/every, finite, paths)

[clairexhuang]

No description provided.

[clairexhuang]

Hey, just creating a PR to merge some definitions & theorems for iTrees, including:

• iflat
• imap
• iexists
• ievery
• ifinite

[binghe]

Just a remind: please fix Unicode violations first.

[mn200]

If you follow the "details" links above you will see how your commit still has Unicode characters and trailing whitespace on some lines. Please replace the former with ASCII equivalents and delete the latter. -- Many thanks!

[binghe]

Additional notes:

1. By adding -t when building HOL, the Unicode violations will be checked (and seen locally) at very early stage.
2. Emacs command delete-trailing-whitespace can be used to remove all trailing whitespaces in the current buffer.
3. In Emacs's HOL->misc menu, there's a command (2nd last) for converting most common Unicode symbols to their ASCII version.

[mn200]

Thank you for your work on this!