---

Step * 1 of Lemma divides_instance


1. TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ Dec(3 | 6)
⊢ 3 | 6
BY
{ Unfold `decidable` 1 }

1
1. TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ (3 | 6) ∨ (¬(3 | 6))
⊢ 3 | 6

---

Latex:

---

Latex:

1.  TERMOF\{decidable\_\_divides\_ext:o,  \mbackslash{}\mbackslash{}v:l\}  3  6  \mmember{}  Dec(3  |  6)
\mvdash{}  3  |  6


By

---

Latex:
Unfold  `decidable`  1

---

Home Index