---

Step * 2 of Lemma all_functionality_wrt_uiff


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. [%2] : ∀x:T. Q[x]
⊢ ∀x:S. P[x]
BY
{ (UseWitness ⌜λx.(snd((p x)))⌝⋅ THEN ProveTrivialWitness)⋅ }

1
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
8. Q x
⊢ snd((p x)) ∈ P x

2
.....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:T ⟶ Q[x]
⊢ istype(S)

---

Latex:

---

Latex:

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.  [\%2]  :  \mforall{}x:T.  Q[x]
\mvdash{}  \mforall{}x:S.  P[x]


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}x.(snd((p  x)))\mkleeneclose{}\mcdot{}  THEN  ProveTrivialWitness)\mcdot{}

---

Home Index