Nuprl Lemma : length-nil

||[]|| 0


Proof




Definitions occuring in Statement :  length: ||as|| nil: [] natural_number: $n sqequal: t
Lemmas referenced :  length_of_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalRule cut lemma_by_obid hypothesis sqequalReflexivity

Latex:
||[]||  \msim{}  0



Date html generated: 2016_05_14-AM-06_33_43
Last ObjectModification: 2015_12_26-PM-00_36_27

Theory : list_0


Home Index