Nuprl Lemma : merge-int_wf

[T:Type]. ∀[as,bs:T List].  (merge-int(as;bs) ∈ List) supposing T ⊆r ℤ


Proof




Definitions occuring in Statement :  merge-int: merge-int(as;bs) list: List uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] member: t ∈ T int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a merge-int: merge-int(as;bs)
Lemmas referenced :  reduce_wf list_wf insert-int_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache intEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (merge-int(as;bs)  \mmember{}  T  List)  supposing  T  \msubseteq{}r  \mBbbZ{}



Date html generated: 2016_05_14-AM-06_30_15
Last ObjectModification: 2015_12_26-PM-00_39_32

Theory : list_0


Home Index