### Nuprl Lemma : dseq_wf

`∀[TypeNames:Type]. ∀[d:DS(TypeNames)]. ∀[a:TypeNames].`
`  (dseq(d;a) ∈ dstype(TypeNames; d; a) ⟶ dstype(TypeNames; d; a) ⟶ 𝔹)`

Proof

Definitions occuring in Statement :  dseq: `dseq(d;a)` dstype: `dstype(TypeNames; d; a)` discrete_struct: `DS(A)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` discrete_struct: `DS(A)` dseq: `dseq(d;a)` dstype: `dstype(TypeNames; d; a)` pi1: `fst(t)` pi2: `snd(t)` subtype_rel: `A ⊆r B` deq: `EqDecider(T)`
Lemmas referenced :  deq_wf discrete_struct_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule applyEquality hypothesisEquality lambdaEquality setElimination rename lemma_by_obid isectElimination hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[TypeNames:Type].  \mforall{}[d:DS(TypeNames)].  \mforall{}[a:TypeNames].
(dseq(d;a)  \mmember{}  dstype(TypeNames;  d;  a)  {}\mrightarrow{}  dstype(TypeNames;  d;  a)  {}\mrightarrow{}  \mBbbB{})

Date html generated: 2016_05_14-PM-03_24_21
Last ObjectModification: 2015_12_26-PM-06_21_42

Theory : decidable!equality

Home Index