Refactor the definition of VLSM inclusions, VLSM equality, etc.

[wkolowski]

The definition of VLSM_incl is pretty awkward, because of the need to share the VLSMType common to both arguments. This causes various issues, including big terms appearing when applying related lemmas, having to manually apply lemmas for symmetry or transitivity, etc. There were some improvements already (PR #193) and some attempted improvements (PR #199), but the situation can still be improved.

Some of the possible tasks include:

• turn VLSM_incl_refl, VLSM_incl_sym and VLSM_incl_trans into instances of Reflexive, Symmetric and Transitive (and likewise for similar lemmas for VLSM_eq, VLSM_embedding, etc.) - this should be the simplest task
• try to come up with an equivalent definition of VLSM_incl based on VLSMMorphism