Nuprl Lemma : sublist*_wf

[T:Type]. ∀[as,bs:T List].  (sublist*(T;as;bs) ∈ ℙ)


Proof




Definitions occuring in Statement :  sublist*: sublist*(T;as;bs) list: List uall: [x:A]. B[x] prop: member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T sublist*: sublist*(T;as;bs) so_lambda: λ2x.t[x] implies:  Q prop: so_apply: x[s]
Lemmas referenced :  all_wf list_wf sublist_wf l_subset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality functionEquality axiomEquality equalityTransitivity equalitySymmetry inhabitedIsType isect_memberEquality universeIsType because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (sublist*(T;as;bs)  \mmember{}  \mBbbP{})



Date html generated: 2019_10_15-AM-10_58_35
Last ObjectModification: 2018_09_27-AM-09_38_55

Theory : list!


Home Index