---

Step * 1 of Lemma listfun_mklist


1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
⊢ (G mklist(x;f)) = mklist(x;λn.G mklist(n + 1;f)[n]) ∈ (B List)
BY
{ (BLemma `list_extensionality` THEN Auto THEN skip{Try ([tactic])})⋅ }

1
1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
9. n : ℕx
⊢ n < ||G mklist(n + 1;f)||

2
1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
⊢ ||G mklist(x;f)|| = ||mklist(x;λn.G mklist(n + 1;f)[n])|| ∈ ℤ

3
1. A : Type
2. B : Type
3. G : (A List) ⟶ (B List)
4. ∀L:A List. (||L|| = ||G L|| ∈ ℕ)
5. ∀L1,L2:A List. ∀i:ℕ.
     ((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B)))
6. f : ℕ ⟶ A
7. x : ℕ
8. ∀x:ℕ. (||G mklist(x;f)|| = x ∈ ℕ)
9. i : ℕ
10. i < ||G mklist(x;f)||
⊢ G mklist(x;f)[i] = mklist(x;λn.G mklist(n + 1;f)[n])[i] ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  G  :  (A  List)  {}\mrightarrow{}  (B  List)
4.  \mforall{}L:A  List.  (||L||  =  ||G  L||)
5.  \mforall{}L1,L2:A  List.  \mforall{}i:\mBbbN{}.
          ((i  \mleq{}  ||L1||)  {}\mRightarrow{}  (i  \mleq{}  ||L2||)  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  (L1[j]  =  L2[j]))  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  (G  L1[j]  =  G  L2[j])))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  A
7.  x  :  \mBbbN{}
8.  \mforall{}x:\mBbbN{}.  (||G  mklist(x;f)||  =  x)
\mvdash{}  (G  mklist(x;f))  =  mklist(x;\mlambda{}n.G  mklist(n  +  1;f)[n])


By

---

Latex:
(BLemma  `list\_extensionality`  THEN  Auto  THEN  skip\{Try  ([tactic])\})\mcdot{}

---

Home Index