---

Step * 1 of Lemma name-morph-satisfies-0'

.....wf..... 
1. I : fset(ℕ)
2. i : ℕ
⊢ (i0) ∈ I+i ⟶ I+i
BY
{ (SubsumeC ⌜I ⟶ I+i⌝⋅ THEN Auto THEN SubtypeReasoning1 THEN EAuto 1) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
\mvdash{}  (i0)  \mmember{}  I+i  {}\mrightarrow{}  I+i


By

---

Latex:
(SubsumeC  \mkleeneopen{}I  {}\mrightarrow{}  I+i\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  SubtypeReasoning1  THEN  EAuto  1)

---

Home Index