---

Step * of Lemma vr_test_foo_bar345566

ℕ7 ⋂ {3..9-} ≡ {3..7-}
BY
{ (RepeatFor 2 (D 0) THENA Auto) }

1
.....subterm..... T:t
1:n
1. x : ℕ7 ⋂ {3..9-}@i
⊢ x ∈ {3..7-}

2
.....subterm..... T:t
1:n
1. x : {3..7-}@i
⊢ x ∈ ℕ7 ⋂ {3..9-}

---

Latex:

---

Latex:
\mBbbN{}7  \mcap{}  \{3..9\msupminus{}\}  \mequiv{}  \{3..7\msupminus{}\}


By

---

Latex:
(RepeatFor  2  (D  0)  THENA  Auto)

---

Home Index