Nuprl Rule : freeFromAtom1Atom2

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:Atom2

  BY freeFromAtom1Atom2 ()

  H  ⊢ x ∈ Atom2

Definitions occuring in rule : free-from-atom: a#x:T, member: t ∈ T, atom: Atom$n, axiom: Ax

Latex:
H \mvdash{} a\#x:Atom2 BY freeFromAtom1Atom2 () H \mvdash{} x \mmember{} Atom2 Date html generated: 2019_06_20-PM-04_12_10 Last ObjectModification: 2015_11_25-PM-03_57_48 Theory : rules Home Index