### Nuprl Lemma : comparison-seq-simple-wf

`∀[T:Type]. ∀[c1,c2:comparison(T)].  (comparison-seq(c1; c2) ∈ comparison(T))`

Proof

Definitions occuring in Statement :  comparison-seq: `comparison-seq(c1; c2)` comparison: `comparison(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` comparison: `comparison(T)` prop: `ℙ` uimplies: `b supposing a` all: `∀x:A. B[x]`
Lemmas referenced :  comparison-seq_wf subtype_rel_comparison equal-wf-T-base comparison_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality isect_memberEquality applyEquality setEquality intEquality setElimination rename hypothesis baseClosed independent_isectElimination lambdaEquality because_Cache sqequalRule axiomEquality equalityTransitivity equalitySymmetry dependent_functionElimination universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[c1,c2:comparison(T)].    (comparison-seq(c1;  c2)  \mmember{}  comparison(T))

Date html generated: 2017_04_17-AM-08_28_22
Last ObjectModification: 2017_02_27-PM-04_49_29

Theory : list_1

Home Index