---

Step * 2 1 1 1 2 1 of Lemma polymorphic-choice-int


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. (f 0 1) = 0 ∈ ℤ
5. x : ℤ
6. y : ℤ
7. (f x y) = y ∈ Base
8. ¬(x = y ∈ ℤ)
9. (f 2 3) = 3 ∈ Base
10. 0 = 3 ∈ (x,y:ℤ//(x ≡ y mod 2))
11. 0 ∈ ℤ
12. 3 ∈ ℤ
13. 0 ≡ 3 mod 2
⊢ (f 2 3) = 2 ∈ Base
BY
{ (RWO "modulus-equal-iff-eqmod<"  (-1) THENA Auto) }

1
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. (f 0 1) = 0 ∈ ℤ
5. x : ℤ
6. y : ℤ
7. (f x y) = y ∈ Base
8. ¬(x = y ∈ ℤ)
9. (f 2 3) = 3 ∈ Base
10. 0 = 3 ∈ (x,y:ℤ//(x ≡ y mod 2))
11. 0 ∈ ℤ
12. 3 ∈ ℤ
13. (0 mod 2) = (3 mod 2) ∈ ℤ
⊢ (f 2 3) = 2 ∈ Base

---

Latex:

---

Latex:

1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
2.  \mforall{}x,y:Base.    (\mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y))
3.  f  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
4.  (f  0  1)  =  0
5.  x  :  \mBbbZ{}
6.  y  :  \mBbbZ{}
7.  (f  x  y)  =  y
8.  \mneg{}(x  =  y)
9.  (f  2  3)  =  3
10.  0  =  3
11.  0  \mmember{}  \mBbbZ{}
12.  3  \mmember{}  \mBbbZ{}
13.  0  \mequiv{}  3  mod  2
\mvdash{}  (f  2  3)  =  2


By

---

Latex:
(RWO  "modulus-equal-iff-eqmod<"    (-1)  THENA  Auto)

---

Home Index