1 2 3 4
(* Testing typing of subst *) Lemma eqType2Set (a b : Set) (H : @eq Type a b) : @eq Set a b. Fail subst.