feat(ModalLogic/LambdaCalculus): modal grind set and proof of type safety for simply typed lambda calculus

[fmontesi]

This PR:

• Introduces a modal grind set for simple modal reasoning. The set does not unfold the meaning of the modal connectives on purpose: it's supposed to be used for quick modal proof search.
• Shows how to use CSLib's modal logic to reason about the PL adage 'safety = progress + preservation'. Once progress and preservation are lifted from existing results into modal propositions, safety follows. The PR also shows how to extract the 'pure' type safety Lean statement.
• Adds a few general properties about relations that were convenient in this development.
• Removes some duplication by aligning uses of 'flip' in Relation and 'Terminating' in modal logic (instead of WellFounded on flip, now it just uses Terminating).

[fmontesi]

All done, @chenson2018, let me know if you'd like to discuss further.

[chenson2018]

For the build issue, you need to add a new exception to scripts/CheckInitImports.lean.

[fmontesi]

For the build issue, you need to add a new exception to scripts/CheckInitImports.lean.

Thanks for the pointer!

[fmontesi]

@chenson2018 all done, thanks for the comments.

[chenson2018]

I cleaned up some changes that were still left over from usage of flip, otherwise this looks good. Thanks!

[fmontesi]

Thank you very much.