2
Definition l1 := let P := 0 in P.
3
Definition l2 := let P := nat in P.
4
Definition l3 := let P := True in P.
5
Definition l4 := let P := Prop in P.
6
Definition l5 := let P := Type in P.
8
(* Check casting of let-in *)
9
Definition l6 := let P := 0:nat in P.
10
Definition l7 := let P := True:Prop in P.
11
Definition l8 := let P := True:Type in P.