Initial support for traits

This adds initial support for traits.

Missing features:

• traits depending on other traits
• generating more specific trait specs for particular instances

These features will be handled in future MRs.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v

@@ -37,6 +37,9 @@ Proof.
     apply lctx_lft_incl_external.
     apply elem_of_cons; right.
     apply elem_of_cons; right.
+    apply elem_of_cons; right.
+    apply elem_of_app; right.
+    apply elem_of_app; right.
     apply elem_of_app; right.
     apply elem_of_app; left.
     unfold_opaque @ty_outlives_E.