### Nuprl Lemma : not-name_eq-implies-sq-bfalse

`∀[hdr1,hdr2:Name].  name_eq(hdr1;hdr2) ~ ff supposing ¬(hdr1 = hdr2 ∈ Name)`

Proof

Definitions occuring in Statement :  name_eq: `name_eq(x;y)` name: `Name` bfalse: `ff` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` sqequal: `s ~ t` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` uiff: `uiff(P;Q)` and: `P ∧ Q` prop: `ℙ` sq_type: `SQType(T)` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}`
Lemmas referenced :  subtype_base_sq bool_subtype_base not_assert_elim name_eq_wf assert-name_eq assert_wf not_wf equal_wf name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination hypothesis hypothesisEquality addLevel impliesFunctionality productElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom sqequalRule isect_memberEquality

Latex:
\mforall{}[hdr1,hdr2:Name].    name\_eq(hdr1;hdr2)  \msim{}  ff  supposing  \mneg{}(hdr1  =  hdr2)

Date html generated: 2016_05_14-PM-03_34_23
Last ObjectModification: 2015_12_26-PM-06_00_20

Theory : decidable!equality

Home Index