Nuprl Lemma : equal-implies-member-param-W
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[p:P]. ∀[w:pW p].
∀[w':pco-W p].
w' ∈ pW p supposing w = w' ∈ (pco-W p)
Proof
Definitions occuring in Statement :
param-W: pW,
param-co-W: pco-W,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_apply: x[s],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
param-W: pW,
all: ∀x:A. B[x],
implies: P ⇒ Q,
squash: ↓T,
prop: ℙ,
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3],
pcw-path: Path,
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
exists: ∃x:A. B[x],
uimplies: b supposing a,
true: True
Lemmas referenced :
param-co-W_wf,
pcw-step-agree_wf,
false_wf,
le_wf,
pcw-path_wf,
all_wf,
squash_wf,
exists_wf,
nat_wf,
pcw-pp-barred_wf,
pcw-partial_wf,
equal_wf,
param-W_wf,
le_reflexive,
true_wf,
pcw-step_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
functionEquality,
cumulativity,
applyEquality,
functionExtensionality,
because_Cache,
lambdaEquality,
universeEquality,
sqequalRule,
setElimination,
rename,
dependent_set_memberEquality,
lambdaFormation,
dependent_functionElimination,
independent_functionElimination,
imageElimination,
imageMemberEquality,
baseClosed,
natural_numberEquality,
independent_pairFormation,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
addLevel,
hyp_replacement,
levelHypothesis,
instantiate
Latex:
\mforall{}[P:Type]. \mforall{}[A:P {}\mrightarrow{} Type]. \mforall{}[B:p:P {}\mrightarrow{} A[p] {}\mrightarrow{} Type]. \mforall{}[C:p:P {}\mrightarrow{} a:A[p] {}\mrightarrow{} B[p;a] {}\mrightarrow{} P]. \mforall{}[p:P].
\mforall{}[w:pW p]. \mforall{}[w':pco-W p].
w' \mmember{} pW p supposing w = w'
Date html generated:
2016_10_21-AM-09_45_34
Last ObjectModification:
2016_07_12-AM-05_05_53
Theory : co-recursion
Home
Index