[TYPES] Inconsistency and non dependent sum elimination

[Param Jyothi Reddy]

Hi,
This is in the context for impredicative Prop and predicative type
hierarchy. The base type system is PTS. I was reading that in presence of
dependent elimination for sum type, elimination from Prop sort to Type sort
can lead to inconsistency in logic. Would it also hold true if we allow only
non-dependent elimination i.e. eliminating Prop into Type without depedency.

SumDependentCase Rule: (inconsistent)
     C[z] : Type   c1[x] : C[Inj_1(x)]   c2[y] : C[Inj_2(y)]   k : A+B
A + B : Prop

----------------------------------------------------------------------------------------------------------------
[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1[x], [y:B]c2[y], [z:A+B]C[z]) : C[k]


SumDependentCase Rule: (consistent??)
     C : Type   c1 : C   c2 : C   k : A+B      A + B : Prop

-----------------------------------------------------------------------------
[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1, [y:B]c2, z:A+B) : C


Would same be true for dependent Sum (Sigma) type? (instead of using direct
second projection, using a case similar to the one given for Sum case).

Thanks in advance,
Param