---

Step * 2 1 of Lemma dl-sem_functionality1

.....antecedent..... 
1. x : ℕ
2. [K] : Type
3. [R] : ℕ ⟶ K ⟶ K ⟶ ℙ
4. [P] : ℕ ⟶ K ⟶ ℙ
5. [P'] : ℕ ⟶ K ⟶ ℙ
6. ∀n:ℕ. ((n ∈ dl-prop-atoms() prop(atm(x))) ⇒ (∀k:K. (P[n] k ⇐⇒ P'[n] k)))
7. dl-kind(prop(atm(x))) = "prop" ∈ Atom
⊢ (x ∈ dl-prop-atoms() prop(atm(x)))
BY
{ ((Unfold `dl-prop-atoms` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbN{}
2.  [K]  :  Type
3.  [R]  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  [P']  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}n:\mBbbN{}.  ((n  \mmember{}  dl-prop-atoms()  prop(atm(x)))  {}\mRightarrow{}  (\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k)))
7.  dl-kind(prop(atm(x)))  =  "prop"
\mvdash{}  (x  \mmember{}  dl-prop-atoms()  prop(atm(x)))


By

---

Latex:
((Unfold  `dl-prop-atoms`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index