Nuprl Lemma : PZF-safe_functionality
∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List. (l_subset(Atom;ws;vs) ⇒ {PZF-safe(phi;vs) ⇒ PZF-safe(phi;ws)})
Proof
Definitions occuring in Statement :
PZF-safe: PZF-safe(phi;vs),
Form: Form(C),
l_subset: l_subset(T;as;bs),
list: T List,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
atom: Atom,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
guard: {T},
PZF-safe: PZF-safe(phi;vs),
uall: ∀[x:A]. B[x]
Lemmas referenced :
FormSafe1_functionality,
list_wf,
Form_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
atomEquality,
universeEquality
Latex:
\mforall{}C:Type. \mforall{}phi:Form(C). \mforall{}vs,ws:Atom List.
(l\_subset(Atom;ws;vs) {}\mRightarrow{} \{PZF-safe(phi;vs) {}\mRightarrow{} PZF-safe(phi;ws)\})
Date html generated:
2018_05_21-PM-11_29_01
Last ObjectModification:
2017_10_12-PM-00_08_36
Theory : PZF
Home
Index