---

Step * of Lemma all_functionality_wrt_uiff

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

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. [%2] : ∀x:S. P[x]
⊢ ∀x:T. Q[x]

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

---

Latex:

---

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


By

---

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

---

Home Index