Nuprl - Proof: select firstn 1

(7steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select firstn 1

T:Type, n:

, as:T List. n

||as||

(

n. firstn(n;as)[i] = as[i])

By:	(CDToVarThen `n' NatInd) THEN (RecCaseSplit `firstn`) THEN (Try (Complete Auto))

Generated subgoal:

1 1. T : Type
2. n :
3. 0<n
4. as:T List. n-1||as||  (i:(n-1). firstn(n-1;as)[i] = as[i])
5. 0<n
  as:T List.
  n||as||

  (i:n. (Case of as; nil  nil ; a.as'  a.firstn(n-1;as'))[i] = as[i])
5 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc