change the deep model of Box<T> to Box<T::DeepModelTy>

[xldenis]

This enables the usage of the derive macro on recursive types. It's absolutely essential that this functions, as for 99% of people deep model should be transparent. I already think that imposing a derive macro quasi-systeatically is already tedious. However, this also suggests that we should change the deep models for other pointer types like Rc or Arc to be Box<T::DeepModel> as well, which, I'm not sure how I feel about that. Finally, I've been thinking we might want to rename DeepModel to EqModel or something which more clearly relates its purpose.

[jhjourdan]

1- Recursive types are not so common
2- I think it is wrong that we need deep-models quasi systematically for every types
3- This changes requires that we add instances of every logical trait for Box

[xldenis]

1- Recursive types are not so common

Not true, honestly, tree structures are very common, especially in verified software.
Moreover, it is not acceptable to just 'bail' completely on these.

2- I think it is wrong that we need deep-models quasi systematically for every types

Again, false, as types quasi-systematically impleemnt PartialEq in Rust which thus requires DeepModel with Creusot.

3- This changes requires that we add instances of every logical trait for Box

No because of auto-deref. If you have OrdLogic for T then Box<T>.cmp will auto-deref in the expected manner.