Step
*
1
1
of Lemma
TR7b
1. [T] : Type
2. [P] : T
3. [C] :
4. x:T. ((P x) C)@i
(x:T. (P x)) C
BY
{ D 4 }
1
1. [T] : Type
2. [P] : T
3. [C] :
4. x : T@i
5. (P x) C@i
(x:T. (P x)) C
Latex:
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. [C] : \mBbbP{}
4. \mexists{}x:T. ((P x) \mwedge{} C)@i
\mvdash{} (\mexists{}x:T. (P x)) \mwedge{} C
By
D 4
Home
Index