Nuprl Lemma : list-ext

`∀[A:Type]. A List ≡ Unit ⋃ (A × (A List))`

Proof

Definitions occuring in Statement :  list: `T List` b-union: `A ⋃ B` ext-eq: `A ≡ B` uall: `∀[x:A]. B[x]` unit: `Unit` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` btrue: `tt` all: `∀x:A. B[x]` implies: `P `` Q` it: `⋅` uiff: `uiff(P;Q)` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` colength: `colength(L)` has-value: `(a)↓`
Lemmas referenced :  colist-ext colist_wf has-value_wf-partial nat_wf set-value-type le_wf int-value-type colength_wf b-union_wf unit_wf2 btrue_wf bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bfalse_wf subtype_partial_sqtype_base set_subtype_base int_subtype_base value-type-has-value subtype_rel_b-union-left subtype_rel_transitivity has-value_wf_base is-exception_wf subtype_rel_b-union-right termination
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_pairFormation productElimination promote_hyp lambdaEquality setEquality cumulativity independent_isectElimination intEquality natural_numberEquality because_Cache productEquality universeEquality setElimination rename hypothesis_subsumption applyEquality imageElimination unionElimination equalityElimination imageMemberEquality dependent_pairEquality lambdaFormation equalityTransitivity equalitySymmetry dependent_pairFormation dependent_functionElimination instantiate independent_functionElimination voidElimination baseClosed independent_pairEquality callbyvalueAdd dependent_set_memberEquality divergentSqle sqleReflexivity addEquality

Latex:
\mforall{}[A:Type].  A  List  \mequiv{}  Unit  \mcup{}  (A  \mtimes{}  (A  List))

Date html generated: 2017_04_14-AM-07_54_14
Last ObjectModification: 2017_02_27-PM-03_21_08

Theory : list_0

Home Index