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