### Nuprl Lemma : req_witness

`∀[x,y:ℝ].  ((x = y) `` (λn.<λ_.Ax, Ax, Ax> ∈ x = y))`

Proof

Definitions occuring in Statement :  req: `x = y` real: `ℝ` uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` lambda: `λx.A[x]` pair: `<a, b>` axiom: `Ax`
Definitions unfolded in proof :  req: `x = y` uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` le: `A ≤ B` and: `P ∧ Q` real: `ℝ` subtype_rel: `A ⊆r B` top: `Top` uimplies: `b supposing a` not: `¬A` prop: `ℙ` guard: `{T}`
Lemmas referenced :  member-not less_than'_wf absval_wf subtract_wf istype-void nat_plus_wf istype-le real_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut lambdaFormation_alt lambdaEquality_alt independent_pairEquality extract_by_obid sqequalHypSubstitution isectElimination thin closedConclusion natural_numberEquality applyEquality setElimination rename because_Cache hypothesis hypothesisEquality isect_memberEquality_alt voidElimination independent_isectElimination universeIsType axiomEquality functionIsType dependent_functionElimination equalityTransitivity equalitySymmetry functionIsTypeImplies inhabitedIsType isectIsTypeImplies productElimination independent_functionElimination

Latex:
\mforall{}[x,y:\mBbbR{}].    ((x  =  y)  {}\mRightarrow{}  (\mlambda{}n.<\mlambda{}\$_{}\$.Ax,  Ax,  Ax>  \mmember{}  x  =  y))

Date html generated: 2019_10_16-PM-03_07_06
Last ObjectModification: 2018_11_08-PM-05_56_58

Theory : reals

Home Index