Nuprl Lemma : comparison_wf

T:Type. (comparison(T) ∈ Type)


Proof




Definitions occuring in Statement :  comparison: comparison(T) all: x:A. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T comparison: comparison(T) and: P ∧ Q uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] prop: implies:  Q
Lemmas referenced :  le_wf equal-wf-T-base equal_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule setEquality functionEquality cumulativity hypothesisEquality because_Cache intEquality productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality applyEquality minusEquality hypothesis baseClosed natural_numberEquality universeEquality

Latex:
\mforall{}T:Type.  (comparison(T)  \mmember{}  Type)



Date html generated: 2016_05_14-PM-02_35_23
Last ObjectModification: 2016_01_15-AM-07_42_30

Theory : list_1


Home Index