Add typeof! to Notations.v (mit-plv#1775)

* Add `subst!` and `typeof!` to `Notations.v`

* Use a version of typeof! that can return `Prop`s and not just `Type`s

* Remove subst! pending a discussion on what syntax makes sense

There's a local version already in Rewrite Rules

src/Util/Notations.v

@@ -205,3 +205,5 @@ Reserved Notation "##### x" (at level 9, x at level 9, format "##### x").
 Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\  x .. y , '//' t").
 (** If we use "( x |? y )", it conflicts with things like [destruct x as [?|?]; ...] *)
 Reserved Notation "( x | ? y )" (format "(  x  | ?  y  )").
+
+Notation "'typeof!' x" := (match x with y => ltac:(let T := type of y in exact T) end) (at level 10, only parsing).