### Nuprl Lemma : comb_for_l_succ_wf

`λT,l,x,P,z. y = succ(x) in l`` P[y] ∈ T:Type ⟶ l:(T List) ⟶ x:T ⟶ P:(T ⟶ ℙ) ⟶ (↓True) ⟶ ℙ`

Proof

Definitions occuring in Statement :  l_succ: l_succ list: `T List` prop: `ℙ` so_apply: `x[s]` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  l_succ_wf squash_wf true_wf istype-universe list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality_alt sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeIsType functionIsType inhabitedIsType universeEquality

Latex:
\mlambda{}T,l,x,P,z.  y  =  succ(x)  in  l{}\mRightarrow{}  P[y]  \mmember{}  T:Type  {}\mrightarrow{}  l:(T  List)  {}\mrightarrow{}  x:T  {}\mrightarrow{}  P:(T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}

Date html generated: 2019_10_15-AM-10_53_16
Last ObjectModification: 2018_10_09-AM-10_31_07

Theory : list!

Home Index