Nuprl Lemma : corec-family_wf

[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].  (corec-family(H) ∈ P ⟶ Type)


Proof




Definitions occuring in Statement :  corec-family: corec-family(H) 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 corec-family: corec-family(H) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  isect-family_wf nat_wf fun_exp_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality instantiate functionEquality cumulativity universeEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[P:Type].  \mforall{}[H:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].    (corec-family(H)  \mmember{}  P  {}\mrightarrow{}  Type)



Date html generated: 2016_05_14-AM-06_12_18
Last ObjectModification: 2015_12_26-PM-00_06_09

Theory : co-recursion


Home Index