### Nuprl Lemma : less_wf

`∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ].  (if (x) < (y)  then a  else b ∈ T)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` member: `t ∈ T` less: `if (a) < (b)  then c  else d` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` less_than: `a < b` and: `P ∧ Q` less_than': `less_than'(a;b)` true: `True` squash: `↓T` top: `Top` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  top_wf less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality lessCases equalityTransitivity hypothesis equalitySymmetry independent_pairFormation sqequalHypSubstitution isectElimination thin baseClosed natural_numberEquality sqequalRule imageMemberEquality axiomSqEquality extract_by_obid isect_memberEquality because_Cache promote_hyp voidElimination voidEquality lambdaFormation imageElimination productElimination axiomEquality intEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:T].  \mforall{}[x,y:\mBbbZ{}].    (if  (x)  <  (y)    then  a    else  b  \mmember{}  T)

Date html generated: 2019_06_20-AM-11_18_55
Last ObjectModification: 2018_08_21-AM-11_05_44

Theory : core_2

Home Index