---

Step * of Lemma all_functionality_wrt_uimplies

∀[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].
  (∀x:T. {Q[x] supposing P[x]}) ⇒ {∀x:T. Q[x] supposing ∀x:S. P[x]} supposing S = T ∈ Type
BY
{ xxx(Unfold `guard` 0 THEN xxx(RepeatFor 7 (xxx(D 0 THENA Auto)xxx) THEN RenameVar `p' (-2))xxx)xxx }

1
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]

---

Latex:

---

Latex:
\mforall{}[S,T:Type].  \mforall{}[P:S  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x:T.  \{Q[x]  supposing  P[x]\})  {}\mRightarrow{}  \{\mforall{}x:T.  Q[x]  supposing  \mforall{}x:S.  P[x]\}  supposing  S  =  T


By

---

Latex:
xxx(Unfold  `guard`  0  THEN  xxx(RepeatFor  7  (xxx(D  0  THENA  Auto)xxx)  THEN  RenameVar  `p'  (-2))xxx)xxx

---

Home Index