New trait encoding scheme and add support for more specific trait impls

This changes the trait encoding scheme to also use the generic encoding from !56 (merged) in order to handle type parameters and lifetime parameters of traits and trait impls correctly.

Along the way, this makes some more changes, such as:

• refactor FunctionSpec so that we can intern it and create references
• refactor spec parsing
• defer normalization of types, as rustc's normalization can't deal with Polonius region variables in Alias

There are some things missing that will be fixed in a future MR:

• correctly export the specifications of impls
• correctly handle lifetime parameters in the translation

case_studies/minivec/src/lib.rs

@@ -394,6 +394,7 @@ impl<T> Vec<T> {
     #[rr::args("(#(<#> xs), γ)", "Z.of_nat i")]
     #[rr::requires("i < length xs")]
     #[rr::observe("γ": "delete i (<#> xs)")]
+    #[rr::returns("xs !!! i")]
     pub fn remove(&mut self, index: usize) -> T {
         // index out of bounds?
         assert!(index < self.len);