Nuprl Rule : freeFromAtomTriviality

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  ⊢ a#x:T

  BY freeFromAtomTriviality ()

     !call_lisp_wargs{NO-UT-OCCURS:t}($n:n x ())
  H  ⊢ x = x ∈ T

Definitions occuring in rule : free-from-atom: a#x:T, equal: s = t ∈ T, axiom: Ax

Latex:
H \mvdash{} a\#x:T BY freeFromAtomTriviality () !call\_lisp\_wargs\{NO-UT-OCCURS:t\}(\$n:n x ()) H \mvdash{} x = x Date html generated: 2019_06_20-PM-04_11_58 Last ObjectModification: 2015_11_25-PM-03_57_48 Theory : rules Home Index