Nuprl Lemma : sq_stable__coW-pos-agree

[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].
  ∀p,q:Pos(coW-game(a.B[a];w;w')).  SqStable(coW-pos-agree(a.B[a];w;w';p;q))


Proof




Definitions occuring in Statement :  coW-pos-agree: coW-pos-agree(a.B[a];w;w';p;q) coW-game: coW-game(a.B[a];w;w') coW: coW(A;a.B[a]) sg-pos: Pos(g) sq_stable: SqStable(P) uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  implies:  Q nat: subtype_rel: A ⊆B so_apply: x[s] so_lambda: λ2x.t[x] and: P ∧ Q prop: member: t ∈ T coW-pos-agree: coW-pos-agree(a.B[a];w;w';p;q) pi1: fst(t) sg-pos: Pos(g) coW-game: coW-game(a.B[a];w;w') all: x:A. B[x] uall: [x:A]. B[x]
Lemmas referenced :  coW_wf coW-game_wf sg-pos_wf sq_stable__copathAgree sq_stable__le copathAgree_wf nat_wf copath-length_wf le_wf sq_stable__and
Rules used in proof :  universeEquality functionEquality cumulativity instantiate dependent_functionElimination independent_functionElimination isect_memberEquality because_Cache rename setElimination hypothesis applyEquality lambdaEquality hypothesisEquality productEquality isectElimination extract_by_obid introduction cut thin productElimination sqequalRule sqequalHypSubstitution lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w,w':coW(A;a.B[a])].
    \mforall{}p,q:Pos(coW-game(a.B[a];w;w')).    SqStable(coW-pos-agree(a.B[a];w;w';p;q))



Date html generated: 2018_07_25-PM-01_43_07
Last ObjectModification: 2018_06_20-PM-02_58_40

Theory : co-recursion


Home Index