Nuprl Lemma : sqntype_subtype

[A,B:Type]. ∀[n:ℕ].  (sqntype(n;A)) supposing (sqntype(n;B) and (A ⊆B))


Definitions occuring in Statement :  sqntype: sqntype(n;T) nat: uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sqntype: sqntype(n;T) all: x:A. B[x] implies:  Q guard: {T} prop:
Lemmas referenced :  equal_functionality_wrt_subtype_rel2 istype-universe base_wf sqntype_wf subtype_rel_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution Error :lambdaFormation_alt,  hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination extract_by_obid isectElimination equalityTransitivity equalitySymmetry independent_isectElimination Error :equalityIsType4,  because_Cache Error :inhabitedIsType,  Error :universeIsType,  sqequalRule Error :lambdaEquality_alt,  Error :axiomSqequalN,  Error :functionIsTypeImplies,  Error :isect_memberEquality_alt,  universeEquality

\mforall{}[A,B:Type].  \mforall{}[n:\mBbbN{}].    (sqntype(n;A))  supposing  (sqntype(n;B)  and  (A  \msubseteq{}r  B))

Date html generated: 2019_06_20-AM-11_34_07
Last ObjectModification: 2018_10_06-AM-11_20_16

Theory : int_1

Home Index