Nuprl Lemma : subtype_rel_record+

[T1,T2:𝕌']. ∀[B1:T1 ⟶ 𝕌']. ∀[B2:T2 ⟶ 𝕌'].
  (∀[z:Atom]. (T1z:B1[self] ⊆T2z:B2[self])) supposing ((∀x:T1. (B1[x] ⊆B2[x])) and (T1 ⊆T2))


Proof




Definitions occuring in Statement :  record+: record+ uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] atom: Atom universe: Type
Definitions unfolded in proof :  record+: record+ uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a so_apply: x[s] bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False subtype_rel: A ⊆B
Lemmas referenced :  dep-isect-subtype2 eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom top_wf subtype_rel_self all_wf subtype_rel_wf subtype_rel_dep_function
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality atomEquality hypothesis lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination because_Cache applyEquality functionExtensionality cumulativity equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination independent_functionElimination voidElimination universeEquality isect_memberFormation axiomEquality isect_memberEquality

Latex:
\mforall{}[T1,T2:\mBbbU{}'].  \mforall{}[B1:T1  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[B2:T2  {}\mrightarrow{}  \mBbbU{}'].
    (\mforall{}[z:Atom].  (T1z:B1[self]  \msubseteq{}r  T2z:B2[self]))  supposing  ((\mforall{}x:T1.  (B1[x]  \msubseteq{}r  B2[x]))  and  (T1  \msubseteq{}r  T2))



Date html generated: 2018_05_21-PM-08_38_32
Last ObjectModification: 2017_07_26-PM-06_02_50

Theory : general


Home Index