### Nuprl Lemma : member-values-for-distinct2

`∀[A,V:Type].  ∀eq:EqDecider(A). ∀L:(A × V) List. ∀v:V.  ((v ∈ values-for-distinct(eq;L)) `` (∃a:A. (<a, v> ∈ L)))`

Proof

Definitions occuring in Statement :  values-for-distinct: `values-for-distinct(eq;L)` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` pair: `<a, b>` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uimplies: `b supposing a` prop: `ℙ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` member: `t ∈ T` values-for-distinct: `values-for-distinct(eq;L)` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` exists: `∃x:A. B[x]` isl: `isl(x)` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  istype-universe deq_wf list_wf values-for-distinct_wf apply-alist_wf unit_wf2 outl_wf list-subtype pi1_wf map_wf remove-repeats_wf l_member_wf member_map member-remove-repeats isl-apply-alist sq_stable_from_decidable assert_wf btrue_wf bfalse_wf decidable__assert
Rules used in proof :  universeEquality instantiate setIsType independent_isectElimination because_Cache rename setElimination universeIsType dependent_functionElimination productIsType hypothesis inhabitedIsType sqequalRule lambdaEquality_alt productEquality hypothesisEquality setEquality thin isectElimination extract_by_obid introduction cut sqequalHypSubstitution lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_functionElimination productElimination dependent_pairFormation_alt hyp_replacement equalitySymmetry applyLambdaEquality independent_pairEquality unionElimination equalityIstype equalityTransitivity imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[A,V:Type].
\mforall{}eq:EqDecider(A).  \mforall{}L:(A  \mtimes{}  V)  List.  \mforall{}v:V.
((v  \mmember{}  values-for-distinct(eq;L))  {}\mRightarrow{}  (\mexists{}a:A.  (<a,  v>  \mmember{}  L)))

Date html generated: 2019_10_15-AM-10_24_20
Last ObjectModification: 2019_08_05-PM-02_03_45

Theory : decidable!equality

Home Index