Nuprl Rule : substitution

H  ⊢ T1[t1/x] ext t

  BY substitution !parameter{i:l} (t1 = t2 ∈ T2) x T1 ()

  H  ⊢ t1 = t2 ∈ T2
  H  ⊢ T1[t2/x] ext t
  H x:T2 ⊢ T1 = T1 ∈ Type

Definitions occuring in rule : equal: s = t ∈ T, universe: Type, axiom: Ax

Latex:
H \mvdash{} T1[t1/x] ext t BY substitution !parameter\{i:l\} (t1 = t2) x T1 () H \mvdash{} t1 = t2 H \mvdash{} T1[t2/x] ext t H x:T2 \mvdash{} T1 = T1 Date html generated: 2016_07_09-AM-08_50_45 Last ObjectModification: 2016_07_08-PM-11_35_12 Theory : rules Home Index