---

Step * 2 of Lemma dl-sem_functionality1


1. x : ℕ
2. [K] : Type
3. [R] : ℕ ⟶ K ⟶ K ⟶ ℙ
4. [P] : ℕ ⟶ K ⟶ ℙ
5. [P'] : ℕ ⟶ K ⟶ ℙ
6. (∀n∈dl-prop-atoms() prop(atm(x)).∀k:K. (P[n] k ⇐⇒ P'[n] k))
7. dl-kind(prop(atm(x))) = "prop" ∈ Atom
⊢ ∀k:K. (P[x] k ⇐⇒ P'[x] k)
BY
{ ((RWO "l_all_iff" (-2) THENA Auto) THEN InstHyp [⌜x⌝] (-2)⋅ THEN Auto) }

1
.....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)))

---

Latex:

---

Latex:

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\mmember{}dl-prop-atoms()  prop(atm(x)).\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
7.  dl-kind(prop(atm(x)))  =  "prop"
\mvdash{}  \mforall{}k:K.  (P[x]  k  \mLeftarrow{}{}\mRightarrow{}  P'[x]  k)


By

---

Latex:
((RWO  "l\_all\_iff"  (-2)  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index