### Nuprl Lemma : decidable__dstype_equal

[A:Type]. ∀a:A. ∀d:DS(A). ∀x,y:dstype(A; d; a).  Dec(x y ∈ dstype(A; d; a))

Proof

Definitions occuring in Statement :  dstype: dstype(TypeNames; d; a) discrete_struct: DS(A) decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  dstype: dstype(TypeNames; d; a) discrete_struct: DS(A) uall: [x:A]. B[x] all: x:A. B[x] pi1: fst(t) member: t ∈ T implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  deq_wf decidable-equal-deq equal_wf pi1_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation productElimination thin sqequalHypSubstitution cut applyEquality functionExtensionality hypothesisEquality cumulativity introduction extract_by_obid isectElimination hypothesis independent_functionElimination dependent_functionElimination equalityTransitivity equalitySymmetry instantiate functionEquality universeEquality lambdaEquality dependent_pairEquality productEquality

Latex:
\mforall{}[A:Type].  \mforall{}a:A.  \mforall{}d:DS(A).  \mforall{}x,y:dstype(A;  d;  a).    Dec(x  =  y)

Date html generated: 2017_04_17-AM-09_09_46
Last ObjectModification: 2017_02_27-PM-05_17_49

Theory : decidable!equality

Home Index