Nuprl Lemma : bunion-value-type

[A,B:Type].  (value-type(A ⋃ B)) supposing (value-type(B) and value-type(A))


Definitions occuring in Statement :  value-type: value-type(T) b-union: A ⋃ B uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a b-union: A ⋃ B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False value-type: value-type(T) has-value: (a)↓
Lemmas referenced :  tunion-value-type bool_wf ifthenelse_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-base b-union_wf base_wf value-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality instantiate hypothesisEquality universeEquality cumulativity independent_isectElimination lambdaFormation unionElimination equalityElimination because_Cache productElimination dependent_pairFormation promote_hyp dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination isect_memberEquality axiomSqleEquality

\mforall{}[A,B:Type].    (value-type(A  \mcup{}  B))  supposing  (value-type(B)  and  value-type(A))

Date html generated: 2017_04_14-AM-07_36_40
Last ObjectModification: 2017_02_27-PM-03_08_58

Theory : subtype_1

Home Index