Nuprl Lemma : iseg_weakening

[T:Type]. ∀l:T List. l ≤ l


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 list: List uall: [x:A]. B[x] all: x:A. B[x] universe: Type
Definitions unfolded in proof :  iseg: l1 ≤ l2 uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] member: t ∈ T prop:
Lemmas referenced :  nil_wf append_back_nil equal_wf list_wf append_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation dependent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache Error :universeIsType,  universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}l:T  List.  l  \mleq{}  l



Date html generated: 2019_06_20-PM-01_28_35
Last ObjectModification: 2018_09_26-PM-05_39_37

Theory : list_1


Home Index