Step
*
1
of Lemma
deq-exists
1. [T] : Type
2. x : EqDecider(T)@i
⊢ ∀x,y:T.  Dec(x = y ∈ T)
BY
{ (UseWitness ⌜deq-witness(x)⌝⋅ THEN Auto) }
Latex:
Latex:
1.  [T]  :  Type
2.  x  :  EqDecider(T)@i
\mvdash{}  \mforall{}x,y:T.    Dec(x  =  y)
By
Latex:
(UseWitness  \mkleeneopen{}deq-witness(x)\mkleeneclose{}\mcdot{}  THEN  Auto)
Home
Index