### Nuprl Lemma : sq_stable__sublist-rec

`∀[T:Type]. ∀l1,l2:T List.  ((∀x,y:T.  Dec(x = y ∈ T)) `` SqStable(sublist-rec(T;l1;l2)))`

Proof

Definitions occuring in Statement :  sublist-rec: `sublist-rec(T;l1;l2)` list: `T List` sq_stable: `SqStable(P)` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  sq_stable_from_decidable sublist-rec_wf decidable__sublist-rec all_wf decidable_wf equal_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination because_Cache sqequalRule lambdaEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2:T  List.    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  SqStable(sublist-rec(T;l1;l2)))

Date html generated: 2016_05_15-PM-03_34_10
Last ObjectModification: 2015_12_27-PM-01_12_58

Theory : general

Home Index