---

Step * 1 1 1 1 of Lemma not-all-finite

.....subterm..... T:t
2:n
1. T : Type
2. P : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. f : T ⟶ ℕk
6. Inj(T;ℕk;f)
7. ∀b:ℕk. ∃a:T. ((f a) = b ∈ ℕk)
8. g : b:ℕk ⟶ T
9. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
10. ∀x:ℕk. P[g x]
11. x : T
12. P[g (f x)]
⊢ x = (g (f x)) ∈ T
BY
{ (BackThruSomeHyp' THEN RWO "-4" 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  k  :  \mBbbN{}
5.  f  :  T  {}\mrightarrow{}  \mBbbN{}k
6.  Inj(T;\mBbbN{}k;f)
7.  \mforall{}b:\mBbbN{}k.  \mexists{}a:T.  ((f  a)  =  b)
8.  g  :  b:\mBbbN{}k  {}\mrightarrow{}  T
9.  \mforall{}b:\mBbbN{}k.  ((f  (g  b))  =  b)
10.  \mforall{}x:\mBbbN{}k.  P[g  x]
11.  x  :  T
12.  P[g  (f  x)]
\mvdash{}  x  =  (g  (f  x))


By

---

Latex:
(BackThruSomeHyp'  THEN  RWO  "-4"  0  THEN  Auto)

---

Home Index