Nuprl Rule : introduction
This rule proved as lemma rule_introduction_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  
H  ⊢ T ext t
  BY introduction t
  
  H  ⊢ t = t ∈ T
Definitions occuring in rule : 
equal: s = t ∈ T
, 
axiom: Ax
Latex:
H    \mvdash{}  T  ext  t
    BY  introduction  t
   
    H    \mvdash{}  t  =  t
Date html generated:
2019_06_20-PM-04_11_41
Last ObjectModification:
2016_07_08-PM-03_48_56
Theory : rules
Home
Index