Nuprl Lemma : pi2_wf

[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (snd(p) ∈ B[fst(p)])


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] so_apply: x[s] pi1: fst(t) pi2: snd(t) member: t ∈ T function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T pi2: snd(t) pi1: fst(t) so_apply: x[s]
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule hypothesisEquality sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry productEquality applyEquality isect_memberEquality isectElimination because_Cache functionEquality cumulativity universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[p:a:A  \mtimes{}  B[a]].    (snd(p)  \mmember{}  B[fst(p)])



Date html generated: 2016_05_13-PM-03_08_26
Last ObjectModification: 2016_01_06-PM-05_27_35

Theory : core_2


Home Index