---

Step * 1 of Lemma lexico_induction

.....antecedent..... 
1. [T] : Type
2. [lt] : T ⟶ T ⟶ ℙ
3. ∀[Q:T ⟶ ℙ]. ((∀b:T. ((∀a:T. (lt[a;b] ⇒ Q[a])) ⇒ Q[b])) ⇒ (∀b:T. Q[b]))@i'
⊢ WellFnd{i}(T;a,b.lt[a;b])
BY
{ (UnfoldTopAb 0 THEN Unfold `guard` 0 THEN Trivial) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  [T]  :  Type
2.  [lt]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}b:T.  ((\mforall{}a:T.  (lt[a;b]  {}\mRightarrow{}  Q[a]))  {}\mRightarrow{}  Q[b]))  {}\mRightarrow{}  (\mforall{}b:T.  Q[b]))@i'
\mvdash{}  WellFnd\{i\}(T;a,b.lt[a;b])


By

---

Latex:
(UnfoldTopAb  0  THEN  Unfold  `guard`  0  THEN  Trivial)

---

Home Index