Step * 2 of Lemma decidable__equal_bag


1. [T] Type
2. ∀x,y:T.  Dec(x y ∈ T)@i
3. xs bag(T)@i
4. ys bag(T)@i
5. EqDecider(T)
⊢ Dec(xs ys ∈ bag(T))
BY
RenameVar `eq' (-1) }

1
1. [T] Type
2. ∀x,y:T.  Dec(x y ∈ T)@i
3. xs bag(T)@i
4. ys bag(T)@i
5. eq EqDecider(T)
⊢ Dec(xs ys ∈ bag(T))


Latex:


Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  xs  :  bag(T)@i
4.  ys  :  bag(T)@i
5.  EqDecider(T)
\mvdash{}  Dec(xs  =  ys)


By


Latex:
RenameVar  `eq'  (-1)




Home Index