Nuprl Rule : freeFromAtomEquality

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  ⊢ a1#x1:T1 = a2#x2:T2 ∈ Type

  BY freeFromAtomEquality ()

  H  ⊢ T1 = T2 ∈ Type
  H  ⊢ x1 = x2 ∈ T1
  H  ⊢ a1 = a2 ∈ Atom$n

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

Latex:
H \mvdash{} a1\#x1:T1 = a2\#x2:T2 BY freeFromAtomEquality () H \mvdash{} T1 = T2 H \mvdash{} x1 = x2 H \mvdash{} a1 = a2 Date html generated: 2019_06_20-PM-04_12_28 Last ObjectModification: 2015_11_25-PM-03_57_47 Theory : rules Home Index