---

Step * 2 1 1 of Lemma lexico_induction


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'
4. [P] : (T List) ⟶ ℙ
5. (∀j:T List. ((∀k:T List. ((k lexico(T; a,b.lt[a;b]) j) ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T List. P[n]}
⊢ (∀L:T List. ((∀L':T List. ((L' lexico(T; a,b.lt[a;b]) L) ⇒ P[L'])) ⇒ P[L])) ⇒ (∀L:T List. P[L])
BY
{ (Unfold `guard` (-1) THEN Trivial) }

---

Latex:

---

Latex:

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'
4.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
5.  (\mforall{}j:T  List.  ((\mforall{}k:T  List.  ((k  lexico(T;  a,b.lt[a;b])  j)  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:T  List.  P[n]\}
\mvdash{}  (\mforall{}L:T  List.  ((\mforall{}L':T  List.  ((L'  lexico(T;  a,b.lt[a;b])  L)  {}\mRightarrow{}  P[L']))  {}\mRightarrow{}  P[L]))  {}\mRightarrow{}  (\mforall{}L:T  List.  P[L])


By

---

Latex:
(Unfold  `guard`  (-1)  THEN  Trivial)

---

Home Index