---

Step * of Lemma lexico_well_fnd

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;a,b.R[a;b]) ⇒ WellFnd{i}(T List;as,bs.as lexico(T; a,b.R[a;b]) bs))
BY
{ xxx(Auto THEN Assert ⌜∀m:ℕ. WellFnd{i}({L:T List| ||L|| = m ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)⌝⋅)xxx }

1
.....assertion..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
⊢ ∀m:ℕ. WellFnd{i}({L:T List| ||L|| = m ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;a,b.R[a;b])
4. ∀m:ℕ. WellFnd{i}({L:T List| ||L|| = m ∈ ℕ} ;as,bs.as lexico(T; a,b.R[a;b]) bs)
⊢ WellFnd{i}(T List;as,bs.as lexico(T; a,b.R[a;b]) bs)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (WellFnd\{i\}(T;a,b.R[a;b])  {}\mRightarrow{}  WellFnd\{i\}(T  List;as,bs.as  lexico(T;  a,b.R[a;b])  bs))


By

---

Latex:
xxx(Auto  THEN  Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  WellFnd\{i\}(\{L:T  List|  ||L||  =  m\}  ;as,bs.as  lexico(T;  a,b.R[a;b])  bs)\mkleeneclose{}\mcdot{})x\000Cxx

---

Home Index