Nuprl Rule : voidElimination
This rule proved as lemma rule_void_elimination_true in file rules/rules_void.v
 at https://github.com/vrahli/NuprlInCoq  
H z:Void, J ⊢ T ext any z
  BY voidElimination #$i
  
  No Subgoals
Definitions occuring in rule : 
void: Void
, 
any: any x
Latex:
H  z:Void,  J  \mvdash{}  T  ext  any  z
    BY  voidElimination  \#\$i
   
    No  Subgoals
Date html generated:
2019_06_20-PM-04_11_46
Last ObjectModification:
2016_07_08-PM-03_48_45
Theory : rules
Home
Index