Add support for dyn

[W95Psp]

From a dependent type perspective, a dyn can be seen as a dependent tuple.
Given a trait Foo, dyn Foo denotes an existentially quantified type: there exists a type that implements trait Foo.

Thus, an inhabitant of dyn Foo is simply a type T, a value of type T, and an impl of Foo for T. In other terms, dyn Foo is t: Type & t & foo t.

Note that Foo (and any trait, actually) should be implemented for such dependent tuples.