### Nuprl Lemma : colist-unfold_wf

`∀[A,B:Type]. ∀[P:B ⟶ (Unit + (A × B))]. ∀[x:B].  (colist-unfold(P;x) ∈ colist(A))`

Proof

Definitions occuring in Statement :  colist-unfold: `colist-unfold(P;x)` colist: `colist(T)` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ⟶ B[x]` product: `x:A × B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` colist-unfold: `colist-unfold(P;x)` colist: `colist(T)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cons: `[a / b]` nil: `[]` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` top: `Top` bfalse: `ff` all: `∀x:A. B[x]` implies: `P `` Q` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  unit_wf2 fix_wf_corec_parameter b-union_wf top_wf it_wf subtype_rel_b-union-left subtype_rel_b-union-right equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry hypothesisEquality isect_memberEquality isectElimination thin because_Cache functionEquality cumulativity unionEquality extract_by_obid productEquality universeEquality lambdaEquality unionElimination equalityElimination functionExtensionality voidElimination voidEquality lambdaFormation applyEquality productElimination independent_pairEquality dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  (Unit  +  (A  \mtimes{}  B))].  \mforall{}[x:B].    (colist-unfold(P;x)  \mmember{}  colist(A))

Date html generated: 2018_05_21-PM-10_20_24
Last ObjectModification: 2017_07_26-PM-06_37_26

Theory : eval!all

Home Index