Nuprl Rule : old_sqequalHypSubstitution
H j:T[a/x] @lvl, J ⊢ C ext t
BY sqequalHypSubstitution #$i (a ~ b) x T
H j:T[a/x] @lvl, J ⊢ a ~ b
H j:T[b/x] @lvl, J ⊢ C ext t
Latex:
H j:T[a/x] @lvl, J \mvdash{} C ext t
BY sqequalHypSubstitution \#\$i (a \msim{} b) x T
H j:T[a/x] @lvl, J \mvdash{} a \msim{} b
H j:T[b/x] @lvl, J \mvdash{} C ext t
Date html generated:
2019_06_20-PM-04_12_16
Last ObjectModification:
2015_11_24-PM-01_52_02
Theory : rules
Home
Index