Nuprl - Pf decidable equal Var

PrintForm Definitions var jlc Sections ClassicalProps(jlc) Doc

At: decidable equal Var

u,v:Var. Dec(u = v)

By: Unfold `Var` 0 THEN UnivCD THEN ProveDecidable

Generated subgoals:

None

About:

PrintForm Definitions var jlc Sections ClassicalProps(jlc) Doc