---

Step * 1 of Lemma all_functionality_wrt_uimplies


1. [S] : Type
2. [T] : Type
3. [P] : S ⟶ ℙ
4. [Q] : T ⟶ ℙ
5. S = T ∈ Type
6. p : ∀x:T. Q[x] supposing P[x]
7. [%2] : ∀x:S. P[x]
⊢ ∀x:T. Q[x]
BY
{ (UseWitness ⌜p⌝⋅ THEN ProveTrivialWitness⋅ THEN Fold `all` (-1)⋅ THEN FunExt⋅ THEN Auto) }

---

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


By

---

Latex:
(UseWitness  \mkleeneopen{}p\mkleeneclose{}\mcdot{}  THEN  ProveTrivialWitness\mcdot{}  THEN  Fold  `all`  (-1)\mcdot{}  THEN  FunExt\mcdot{}  THEN  Auto)

---

Home Index