Nuprl Rule : exceptionSqequal
This rule proved as lemma rule_exception_sqequal_true in file rules/rules_exception.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ C ext c
  BY exceptionSqequal x u v t ()
  
  H  ⊢ is-exception(t)
  H [u:Base], [v:Base], [x:(t ~ exception(u; v))] ⊢ C ext c
  H u:Base, v:Base ⊢ t ∈ Base
Definitions occuring in rule : 
is-exception: is-exception(t)
, 
sqequal: s ~ t
, 
member: t ∈ T
, 
base: Base
, 
axiom: Ax
Latex:
H    \mvdash{}  C  ext  c
    BY  exceptionSqequal  x  u  v  t  ()
   
    H    \mvdash{}  is-exception(t)
    H  [u:Base],  [v:Base],  [x:(t  \msim{}  exception(u;  v))]  \mvdash{}  C  ext  c
    H  u:Base,  v:Base  \mvdash{}  t  \mmember{}  Base
Date html generated:
2019_06_20-PM-04_11_49
Last ObjectModification:
2016_07_08-PM-03_48_58
Theory : rules
Home
Index