Predicativity for Pi in turnstile-core

[wilbowma]

Currently allows impredicativity at all levels, which is inconsistent

Need the following rules:

⊢ A : Type i
x,A ⊢ B : Type 0
--------------- Prod-Prop
⊢ Πx:A.B : Type 0

⊢ A : Type j
x,A ⊢ B : Type i
--------------- Prod-Type
⊢ Πx:A.B : Type (max i j)

Alternative Prod-Type using subtyping

⊢ A : Type i
x,A ⊢ B : Type i
--------------- Prod-Type
⊢ Πx:A.B : Type i

[stchang]

fixed by #21