Nuprl Lemma : FormSafe1-iff-FormSafe1''
∀C:Type. ∀f:Form(C). ∀vs:Atom List. (FormSafe1(f) vs ⇐⇒ FormSafe1''(f) vs)
Proof
Definitions occuring in Statement :
FormSafe1'': FormSafe1''(f),
FormSafe1: FormSafe1(f),
Form: Form(C),
list: T List,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
atom: Atom,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
FormSafe1''_wf,
list_wf,
Form_wf,
FormSafe1'-iff-FormSafe1'',
FormSafe1'_wf,
all_wf,
iff_wf,
FormSafe-iff-FormSafe1',
FormSafe1_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
independent_pairFormation,
hypothesis,
applyEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
because_Cache,
atomEquality,
universeEquality,
addLevel,
allFunctionality,
productElimination,
impliesFunctionality,
dependent_functionElimination,
independent_functionElimination,
lambdaEquality,
sqequalRule,
instantiate
Latex:
\mforall{}C:Type. \mforall{}f:Form(C). \mforall{}vs:Atom List. (FormSafe1(f) vs \mLeftarrow{}{}\mRightarrow{} FormSafe1''(f) vs)
Date html generated:
2018_05_21-PM-11_30_03
Last ObjectModification:
2017_10_12-PM-03_55_28
Theory : PZF
Home
Index