Nuprl Lemma : is-above-subtype

[A,B:Type].  ∀[a:A]. ∀[z:Base].  (is-above(A;a;z)  is-above(B;a;z)) supposing A ⊆B


Proof




Definitions occuring in Statement :  is-above: is-above(T;a;z) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] implies:  Q base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T subtype_rel: A ⊆B implies:  Q is-above: is-above(T;a;z) exists: x:A. B[x] and: P ∧ Q prop: cand: c∧ B guard: {T}
Lemmas referenced :  is-above_wf base_wf subtype_rel_wf equal_functionality_wrt_subtype_rel2 equal-wf-base-T sqle_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule axiomEquality hypothesis thin rename lambdaFormation sqequalHypSubstitution productElimination lemma_by_obid isectElimination hypothesisEquality universeEquality dependent_pairFormation equalityTransitivity equalitySymmetry independent_isectElimination independent_functionElimination independent_pairFormation productEquality applyEquality

Latex:
\mforall{}[A,B:Type].    \mforall{}[a:A].  \mforall{}[z:Base].    (is-above(A;a;z)  {}\mRightarrow{}  is-above(B;a;z))  supposing  A  \msubseteq{}r  B



Date html generated: 2016_05_13-PM-04_13_02
Last ObjectModification: 2015_12_26-AM-11_11_22

Theory : subtype_1


Home Index