### Nuprl Lemma : comb_for_mset_mem_wf

`λs,x,a,z. (x ∈b a) ∈ s:DSet ⟶ x:|s| ⟶ a:MSet{s} ⟶ (↓True) ⟶ 𝔹`

Proof

Definitions occuring in Statement :  mset_mem: mset_mem mset: `MSet{s}` bool: `𝔹` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` dset: `DSet`
Lemmas referenced :  mset_mem_wf squash_wf true_wf mset_wf set_car_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid dependent_functionElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry isectElimination setElimination rename

Latex:
\mlambda{}s,x,a,z.  (x  \mmember{}\msubb{}  a)  \mmember{}  s:DSet  {}\mrightarrow{}  x:|s|  {}\mrightarrow{}  a:MSet\{s\}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}

Date html generated: 2016_05_16-AM-07_47_12
Last ObjectModification: 2015_12_28-PM-06_03_33

Theory : mset

Home Index