---

Step * of Lemma ppcc-test2

∀[T:Type]
  ∀f:T ⟶ T
    ∀[Q:T ⟶ ℙ]. ∀[P:T ⟶ T ⟶ ℙ].  ((∀z:T. (Q[z] ⇒ P[z;f[z]])) ⇒ (∀x,y:T.  Q[x] ⇒ P[x;y] supposing y = f[x] ∈ T))
BY
{ (UnivCD THENA Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. [Q] : T ⟶ ℙ
4. [P] : T ⟶ T ⟶ ℙ
5. ∀z:T. (Q[z] ⇒ P[z;f[z]])
6. x : T
7. y : T
8. y = f[x] ∈ T
9. Q[x]
⊢ P[x;y]

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index