---

Step * 1 2 1 1 of Lemma injection-inverse


1. A : Type
2. B : Type
3. f : A →⟶ B@i
4. a : A@i
5. n : ℕ@i
6. h : ℕn ⟶ A@i
7. Surj(ℕn;A;h)@i
8. ∀x,y:B.  Dec(x = y ∈ B)@i
9. test : b:B ⟶ (∃i:ℕn. ((f (h i)) = b ∈ B) + (¬(∃i:ℕn. ((f (h i)) = b ∈ B))))
10. a@0 : A@i
⊢ case test (f a@0) of inl(e) => h (fst(e)) | inr(z) => a = a@0 ∈ A
BY
{ (GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. f : A →⟶ B@i
4. a : A@i
5. n : ℕ@i
6. h : ℕn ⟶ A@i
7. Surj(ℕn;A;h)@i
8. ∀x,y:B.  Dec(x = y ∈ B)@i
9. test : b:B ⟶ (∃i:ℕn. ((f (h i)) = b ∈ B) + (¬(∃i:ℕn. ((f (h i)) = b ∈ B))))
10. a@0 : A@i
11. x : ∃i:ℕn. ((f (h i)) = (f a@0) ∈ B)@i
12. (test (f a@0)) = (inl x) ∈ (∃i:ℕn. ((f (h i)) = (f a@0) ∈ B) + (¬(∃i:ℕn. ((f (h i)) = (f a@0) ∈ B))))@i
⊢ (h (fst(x))) = a@0 ∈ A

2
1. A : Type
2. B : Type
3. f : A →⟶ B@i
4. a : A@i
5. n : ℕ@i
6. h : ℕn ⟶ A@i
7. Surj(ℕn;A;h)@i
8. ∀x,y:B.  Dec(x = y ∈ B)@i
9. test : b:B ⟶ (∃i:ℕn. ((f (h i)) = b ∈ B) + (¬(∃i:ℕn. ((f (h i)) = b ∈ B))))
10. a@0 : A@i
11. y : ¬(∃i:ℕn. ((f (h i)) = (f a@0) ∈ B))@i
12. (test (f a@0)) = (inr y ) ∈ (∃i:ℕn. ((f (h i)) = (f a@0) ∈ B) + (¬(∃i:ℕn. ((f (h i)) = (f a@0) ∈ B))))@i
⊢ a = a@0 ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  \mrightarrow{}{}\mrightarrow{}  B@i
4.  a  :  A@i
5.  n  :  \mBbbN{}@i
6.  h  :  \mBbbN{}n  {}\mrightarrow{}  A@i
7.  Surj(\mBbbN{}n;A;h)@i
8.  \mforall{}x,y:B.    Dec(x  =  y)@i
9.  test  :  b:B  {}\mrightarrow{}  (\mexists{}i:\mBbbN{}n.  ((f  (h  i))  =  b)  +  (\mneg{}(\mexists{}i:\mBbbN{}n.  ((f  (h  i))  =  b))))
10.  a@0  :  A@i
\mvdash{}  case  test  (f  a@0)  of  inl(e)  =>  h  (fst(e))  |  inr(z)  =>  a  =  a@0


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index