Nuprl Lemma : seq-nil-len
||seq-nil()|| ~ 0
Proof
Definitions occuring in Statement : 
seq-nil: seq-nil()
, 
seq-len: ||s||
, 
natural_number: $n
, 
sqequal: s ~ t
Definitions unfolded in proof : 
seq-nil: seq-nil()
, 
pi1: fst(t)
, 
seq-len: ||s||
Rules used in proof : 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalRule, 
sqequalSubstitution
Latex:
||seq-nil()||  \msim{}  0
Date html generated:
2018_07_25-PM-01_29_27
Last ObjectModification:
2018_06_18-PM-02_00_36
Theory : arithmetic
Home
Index