Nuprl Lemma : coW-equiv_inversion
∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). (coW-equiv(a.B[a];w;w') ⇒ coW-equiv(a.B[a];w';w))
Proof
Definitions occuring in Statement :
coW-equiv: coW-equiv(a.B[a];w;w'),
coW: coW(A;a.B[a]),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
coW-equiv: coW-equiv(a.B[a];w;w'),
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
isom-games: g1 ≅ g2,
exists: ∃x:A. B[x],
sg-pos: Pos(g),
pi1: fst(t),
coW-game: coW-game(a.B[a];w;w'),
and: P ∧ Q,
sg-legal1: Legal1(x;y),
pi2: snd(t),
or: P ∨ Q,
guard: {T},
cand: A c∧ B,
subtype_rel: A ⊆r B,
nat: ℕ,
sg-legal2: Legal2(x;y),
sg-init: InitialPos(g)
Lemmas referenced :
isom-preserves-win2,
coW-game_wf,
coW-equiv_wf,
coW_wf,
sg-pos_wf,
equal_wf,
copath-length_wf,
nat_wf,
copathAgree_wf,
copath_wf,
sg-legal1_wf,
sg-legal2_wf,
sg-init_wf,
all_wf,
exists_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
cut,
introduction,
extract_by_obid,
dependent_functionElimination,
thin,
isectElimination,
hypothesisEquality,
sqequalRule,
lambdaEquality,
applyEquality,
hypothesis,
independent_functionElimination,
instantiate,
cumulativity,
functionEquality,
universeEquality,
dependent_pairFormation,
spreadEquality,
productElimination,
independent_pairEquality,
independent_pairFormation,
unionElimination,
inrFormation,
productEquality,
intEquality,
setElimination,
rename,
addEquality,
because_Cache,
natural_numberEquality,
inlFormation,
equalitySymmetry,
functionExtensionality,
equalityTransitivity
Latex:
\mforall{}[A:\mBbbU{}']. \mforall{}B:A {}\mrightarrow{} Type. \mforall{}w,w':coW(A;a.B[a]). (coW-equiv(a.B[a];w;w') {}\mRightarrow{} coW-equiv(a.B[a];w';w))
Date html generated:
2018_07_25-PM-01_42_46
Last ObjectModification:
2018_07_11-PM-00_02_58
Theory : co-recursion
Home
Index