Nuprl Rule : freeFromAtomAbsurdity
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
 at https://github.com/vrahli/NuprlInCoq  
H z:a#a:Atom$n, J ⊢ T ext any z
  BY freeFromAtomAbsurdity #$i
  
  No Subgoals
Definitions occuring in rule : 
free-from-atom: a#x:T
, 
atom: Atom$n
, 
any: any x
Latex:
H  z:a\#a:Atom\$n,  J  \mvdash{}  T  ext  any  z
    BY  freeFromAtomAbsurdity  \#\$i
   
    No  Subgoals
Date html generated:
2019_06_20-PM-04_11_58
Last ObjectModification:
2015_11_25-PM-03_57_48
Theory : rules
Home
Index