Nuprl Lemma : sq_stable__l_subset
∀[T:Type]. ∀[L1:T List]. ∀L2:T List. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ SqStable(l_subset(T;L1;L2)))
Proof
Definitions occuring in Statement :
l_subset: l_subset(T;as;bs),
list: T List,
sq_stable: SqStable(P),
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
l_subset: l_subset(T;as;bs),
sq_stable: SqStable(P),
member: t ∈ T,
decidable: Dec(P),
or: P ∨ Q,
squash: ↓T,
false: False,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
guard: {T},
not: ¬A
Lemmas referenced :
decidable__l_member,
l_member_wf,
squash_wf,
all_wf,
decidable_wf,
equal_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
dependent_functionElimination,
hypothesisEquality,
independent_functionElimination,
hypothesis,
unionElimination,
imageElimination,
voidElimination,
sqequalRule,
lambdaEquality,
functionEquality,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[L1:T List]. \mforall{}L2:T List. ((\mforall{}x,y:T. Dec(x = y)) {}\mRightarrow{} SqStable(l\_subset(T;L1;L2)))
Date html generated:
2016_05_14-AM-07_54_07
Last ObjectModification:
2015_12_26-PM-04_48_19
Theory : list_1
Home
Index