---

Step * 2 2 1 1 1 of Lemma decidable__exists_length

.....subterm..... T:t
2:n
1. T : Type
2. P : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
7. f : {as:T List| ||as|| = n ∈ ℤ}  ⟶ ℕk^n
8. Inj({as:T List| ||as|| = n ∈ ℤ} ;ℕk^n;f)
9. ∀b:ℕk^n. ∃a:{as:T List| ||as|| = n ∈ ℤ} . ((f a) = b ∈ ℕk^n)
10. g : b:ℕk^n ⟶ {as:T List| ||as|| = n ∈ ℤ} 
11. ∀b:ℕk^n. ((f (g b)) = b ∈ ℕk^n)
12. L : T List
13. ||L|| = n ∈ ℤ
14. P[L]
⊢ (g (f L)) = L ∈ (T List)
BY
{ (BackThruSomeHyp' THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(BackThruSomeHyp'  THEN  Auto)

---

Home Index