---

Step * 1 2 of Lemma all_functionality_wrt_uiff

.....wf..... 
1. S : Type
2. T : Type
3. P : S ⟶ ℙ
4. Q : T ⟶ ℙ
5. S = T ∈ Type
6. p : ∀x:T. uiff(P[x];Q[x])
7. x:S ⟶ P[x]
⊢ istype(T)
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  S  :  Type
2.  T  :  Type
3.  P  :  S  {}\mrightarrow{}  \mBbbP{}
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
5.  S  =  T
6.  p  :  \mforall{}x:T.  uiff(P[x];Q[x])
7.  x:S  {}\mrightarrow{}  P[x]
\mvdash{}  istype(T)


By

---

Latex:
Auto

---

Home Index