Nuprl Lemma : pi1_wf

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

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` so_apply: `x[s]` pi1: `fst(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` 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]].    (fst(p)  \mmember{}  A)

Date html generated: 2016_05_13-PM-03_08_28
Last ObjectModification: 2016_01_06-PM-05_27_33

Theory : core_2

Home Index