---

Step * 2 of Lemma deq-fset_wf


1. T : Type
2. eq : EqDecider(T)
⊢ λx,y. isl(TERMOF{decidable__equal_fset:o, \\v:l, i:l} eq x y) ∈ EqDecider(fset(T))
BY
{ (MemTypeCD
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (((MemCD THENA Auto) ORELSE (D 0 THENA Auto)))
   THEN GenConcl ⌜(TERMOF{decidable__equal_fset:o, \\v:l, i:l} eq x y) = d ∈ Dec(x = y ∈ fset(T))⌝⋅
   THEN Auto
   THEN Try ((GenConclAtAddrType ⌜∀xs,ys:fset(T).  Dec(xs = ys ∈ fset(T))⌝ [2;1;1]⋅ THEN Auto))
   THEN DVar `d'
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mlambda{}x,y.  isl(TERMOF\{decidable\_\_equal\_fset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  eq  x  y)  \mmember{}  EqDecider(fset(T))


By

---

Latex:
(MemTypeCD
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (((MemCD  THENA  Auto)  ORELSE  (D  0  THENA  Auto)))
  THEN  GenConcl  \mkleeneopen{}(TERMOF\{decidable\_\_equal\_fset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  eq  x  y)  =  d\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  ((GenConclAtAddrType  \mkleeneopen{}\mforall{}xs,ys:fset(T).    Dec(xs  =  ys)\mkleeneclose{}  [2;1;1]\mcdot{}  THEN  Auto))
  THEN  DVar  `d'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index