Nuprl Lemma : decidable__equal_Kind
∀a,b:Knd. Dec(a = b ∈ Knd)
Proof
Definitions occuring in Statement :
Knd: Knd,
decidable: Dec(P),
all: ∀x:A. B[x],
equal: s = t ∈ T
Lemmas :
decidable__assert,
eq_knd_wf,
Knd_wf,
equal_wf,
assert_wf,
all_wf,
decidable_wf
\mforall{}a,b:Knd. Dec(a = b)
Date html generated:
2015_07_17-AM-09_13_07
Last ObjectModification:
2015_01_28-AM-07_55_33
Home
Index