Nuprl Rule : token1Equality
H ⊢ '$x'1 = '$x'1 ∈ Atom1
BY token1Equality ()
No Subgoals
Definitions occuring in rule :
equal: s = t ∈ T,
atom: Atom$n,
token: '$x'1,
axiom: Ax
Latex:
H \mvdash{} '\$x'1 = '\$x'1
BY token1Equality ()
No Subgoals
Date html generated:
2019_06_20-PM-04_12_07
Last ObjectModification:
2015_11_25-PM-03_55_41
Theory : rules
Home
Index