Nuprl Lemma : tl_wf

[A:Type]. ∀[l:A List].  (tl(l) ∈ List)


Proof




Definitions occuring in Statement :  tl: tl(l) list: List uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] or: P ∨ Q cons: [a b] top: Top
Lemmas referenced :  list-cases reduce_tl_nil_lemma nil_wf product_subtype_list reduce_tl_cons_lemma istype-void list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis dependent_functionElimination unionElimination sqequalRule promote_hyp hypothesis_subsumption productElimination Error :isect_memberEquality_alt,  voidElimination axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  because_Cache universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].    (tl(l)  \mmember{}  A  List)



Date html generated: 2019_06_20-PM-00_38_39
Last ObjectModification: 2018_10_08-PM-04_45_43

Theory : list_0


Home Index