### Nuprl Lemma : equal-valueall-type

`∀[T:Type]. ∀[x,y:T].  valueall-type(x = y ∈ T)`

Proof

Definitions occuring in Statement :  valueall-type: `valueall-type(T)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` valueall-type: `valueall-type(T)` uimplies: `b supposing a` sq_stable: `SqStable(P)` implies: `P `` Q` all: `∀x:A. B[x]` has-value: `(a)↓` prop: `ℙ` squash: `↓T`
Lemmas referenced :  sq_stable__has-value evalall-axiom has-value_wf_base is-exception_wf equal_wf equal-wf-base base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule baseApply closedConclusion baseClosed hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry because_Cache lambdaFormation equalityElimination divergentSqle sqleReflexivity dependent_functionElimination imageMemberEquality imageElimination cumulativity isect_memberEquality axiomSqleEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].    valueall-type(x  =  y)

Date html generated: 2017_04_14-AM-07_15_29
Last ObjectModification: 2017_02_27-PM-02_50_50

Theory : call!by!value_1

Home Index