---

Step * of Lemma rel_plus-uniform-TI

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  ((∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R+ x y;x.Q[x])) ⇒ (∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R[x;y];x.Q[x])))
BY
{ (Auto THEN D 0 THEN Auto THEN BackThruHyp' 3 THEN Auto THEN BackThruHyp' 5 THEN Auto THEN BackThruSomeHyp) }

1
.....wf..... 
1. T : Type@i'
2. R : T ⟶ T ⟶ ℙ@i'
3. ∀Q:T ⟶ ℙ. ((∀[x:T]. ((∀[s:{s:T| R+ x s} ]. Q[s]) ⇒ Q[x])) ⇒ (∀[x:T]. (Q x)))@i'
4. Q : T ⟶ ℙ@i'
5. ∀[x:T]. ((∀[s:{s:T| R[x;s]} ]. Q[s]) ⇒ Q[x])@i
6. x : T
7. x1 : T
8. ∀[s:{s:T| R+ x1 s} ]. Q[s]@i
9. s : {s:T| R[x1;s]} 
⊢ s ∈ {s:T| R+ x1 s} 

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  uniform-TI(T;x,y.R\msupplus{}  x  y;x.Q[x]))  {}\mRightarrow{}  (\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  uniform-TI(T;x,y.R[x;y];x.Q[x])))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  BackThruHyp'  3
  THEN  Auto
  THEN  BackThruHyp'  5
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index