---

Step * 1 of Lemma free-from-atom_wf_general


1. [T] : Type
2. [x] : T
⊢ ∀[a:Atom$m]. (a#x:T ∈ ℙ)
BY
{ D 0 }

1
1. T : Type
2. x : T
3. a : Atom$m
⊢ a#x:T ∈ ℙ

2
.....wf..... 
1. T : Type
2. x : T
⊢ istype(Atom$m)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [x]  :  T
\mvdash{}  \mforall{}[a:Atom\$m].  (a\#x:T  \mmember{}  \mBbbP{})


By

---

Latex:
D  0

---

Home Index