---

Step * of Lemma member-fset-pair

∀[T:Type]. ∀eq:EqDecider(T). ∀x,y,z:T.  uiff(z ∈ {x,y};(z = x ∈ T) ∨ (z = y ∈ T))
BY
{ (((UnivCD THENA Auto) THEN (InstLemma `deq-implies` [⌜T⌝]⋅ THENA Auto))
   THEN RepUR ``fset-member fset-pair eqof`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Auto) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
5. z : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. [%] : (x = z ∈ T) ∨ (y = z ∈ T) ∨ False
⊢ (z = x ∈ T) ∨ (z = y ∈ T)

2
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
5. z : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. [%] : (z = x ∈ T) ∨ (z = y ∈ T)
⊢ (x = z ∈ T) ∨ (y = z ∈ T) ∨ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x,y,z:T.    uiff(z  \mmember{}  \{x,y\};(z  =  x)  \mvee{}  (z  =  y))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (InstLemma  `deq-implies`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  RepUR  ``fset-member  fset-pair  eqof``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto)

---

Home Index