---

Step * 1 1 of Lemma fset-filter_wf


1. T : Type
2. P : T ⟶ 𝔹
3. s : Base
4. s1 : Base
5. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
6. s ∈ T List
7. s1 ∈ T List
8. t : T@i
9. (t ∈ s) ⇐⇒ (t ∈ s1)
⊢ (t ∈ s) ∧ (↑P[t]) ⇐⇒ (t ∈ s1) ∧ (↑P[t])
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  s  :  Base
4.  s1  :  Base
5.  s  =  s1
6.  s  \mmember{}  T  List
7.  s1  \mmember{}  T  List
8.  t  :  T@i
9.  (t  \mmember{}  s)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  s1)
\mvdash{}  (t  \mmember{}  s)  \mwedge{}  (\muparrow{}P[t])  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  s1)  \mwedge{}  (\muparrow{}P[t])


By

---

Latex:
Auto

---

Home Index