Nuprl Lemma : strong-subtype-dep-product
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
(strong-subtype(a:A × B[a];c:C × D[c])) supposing ((∀a:A. strong-subtype(B[a];D[a])) and strong-subtype(A;C))
Proof
Definitions occuring in Statement :
strong-subtype: strong-subtype(A;B),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
implies: P ⇒ Q,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
strong-subtype: strong-subtype(A;B),
cand: A c∧ B,
prop: ℙ,
so_lambda: λ2x.t[x],
exists: ∃x:A. B[x],
pi1: fst(t),
pi2: snd(t),
label: ...$L... t
Lemmas referenced :
strong-subtype-implies,
strong-subtype_witness,
strong-subtype_wf,
istype-universe,
pi1_wf,
pi2_wf,
subtype_rel_product
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
independent_functionElimination,
hypothesis,
productEquality,
applyEquality,
sqequalRule,
Error :functionIsType,
Error :universeIsType,
productElimination,
Error :isect_memberEquality_alt,
because_Cache,
Error :isectIsTypeImplies,
Error :inhabitedIsType,
instantiate,
universeEquality,
independent_pairFormation,
lemma_by_obid,
lambdaEquality,
independent_isectElimination,
lambdaFormation,
dependent_functionElimination,
Error :lambdaEquality_alt,
Error :setIsType,
Error :productIsType,
Error :equalityIstype,
setElimination,
rename,
Error :dependent_set_memberEquality_alt,
Error :dependent_pairFormation_alt,
applyLambdaEquality,
Error :dependent_pairEquality_alt,
equalityTransitivity,
equalitySymmetry,
hyp_replacement
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[C:Type]. \mforall{}[D:C {}\mrightarrow{} Type].
(strong-subtype(a:A \mtimes{} B[a];c:C \mtimes{} D[c])) supposing
((\mforall{}a:A. strong-subtype(B[a];D[a])) and
strong-subtype(A;C))
Date html generated:
2019_06_20-PM-00_27_57
Last ObjectModification:
2018_12_16-PM-00_26_22
Theory : subtype_1
Home
Index