---

Step * of Lemma rel_plus-TI

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  ((∀Q:T ⟶ ℙ. TI(T;x,y.R+ x y;x.Q[x])) ⇒ (∀Q:T ⟶ ℙ. 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@i
7. x1 : T@i
8. ∀s:{s:T| R+ x1 s} . Q[s]@i
9. s : {s:T| R[x1;s]} @i
⊢ s ∈ {s:T| R+ x1 s} 

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  TI(T;x,y.R\msupplus{}  x  y;x.Q[x]))  {}\mRightarrow{}  (\mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  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