Nuprl Lemma : bunion-valueall-type

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


Proof




Definitions occuring in Statement :  valueall-type: valueall-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 valueall-type: valueall-type(T) has-value: (a)↓
Lemmas referenced :  tunion-valueall-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 valueall-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

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



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

Theory : subtype_1


Home Index