Nuprl Rule : thin
This rule proved as lemma rule_thin_true in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  
H x:A, J ⊢ T ext t
  BY thin #$i
  
  H J ⊢ T ext t
Latex:
H  x:A,  J  \mvdash{}  T  ext  t
    BY  thin  \#\$i
   
    H  J  \mvdash{}  T  ext  t
Date html generated:
2019_06_20-PM-04_11_40
Last ObjectModification:
2016_07_08-PM-03_48_46
Theory : rules
Home
Index