---

Step * of Lemma deq-f-subset_wf

∀[T:Type]. ∀[eq:EqDecider(T)].  (deq-f-subset(eq) ∈ {d:fset(T) ⟶ fset(T) ⟶ 𝔹| ∀x,y:fset(T).  (x ⊆ y ⇐⇒ ↑(d x y))} )
BY
{ (Auto
   THEN Unfold `deq-f-subset` 0
   THEN Subst' TERMOF{decidable__f-subset:o, 1:l, 1:l} ~ TERMOF{decidable__f-subset:o, \\v:l, i:l} 0) }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
⊢ TERMOF{decidable__f-subset:o, 1:l, 1:l} ~ TERMOF{decidable__f-subset:o, \\v:l, i:l}

2
1. T : Type
2. eq : EqDecider(T)
⊢ λx,y. isl(TERMOF{decidable__f-subset:o, \\v:l, i:l} eq x y) ∈ {d:fset(T) ⟶ fset(T) ⟶ 𝔹| 
                                                             ∀x,y:fset(T).  (x ⊆ y ⇐⇒ ↑(d x y))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
    (deq-f-subset(eq)  \mmember{}  \{d:fset(T)  {}\mrightarrow{}  fset(T)  {}\mrightarrow{}  \mBbbB{}|  \mforall{}x,y:fset(T).    (x  \msubseteq{}  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  x  y))\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `deq-f-subset`  0
  THEN  Subst'  TERMOF\{decidable\_\_f-subset:o,  1:l,  1:l\}  \msim{}  TERMOF\{decidable\_\_f-subset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  0)

---

Home Index