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