Nuprl Lemma : iseg-subtype
∀[A,B:Type]. ∀xs,ys:A List. {xs ≤ ys ⇒ xs ≤ ys} supposing strong-subtype(A;B)
Proof
Definitions occuring in Statement :
iseg: l1 ≤ l2,
list: T List,
strong-subtype: strong-subtype(A;B),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
implies: P ⇒ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
strong-subtype: strong-subtype(A;B),
cand: A c∧ B,
iseg: l1 ≤ l2,
exists: ∃x:A. B[x],
squash: ↓T,
label: ...$L... t,
true: True,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
strong-subtype_witness,
iseg_wf,
subtype_rel_list,
strong-subtype_wf,
list_wf,
strong-subtype-equal-lists,
nth_tl_wf,
length_wf,
equal_wf,
nth_tl_append,
squash_wf,
true_wf,
append_wf,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
independent_functionElimination,
hypothesis,
rename,
cumulativity,
applyEquality,
because_Cache,
independent_isectElimination,
productElimination,
universeEquality,
equalityTransitivity,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality,
dependent_pairFormation,
lambdaEquality,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[A,B:Type]. \mforall{}xs,ys:A List. \{xs \mleq{} ys {}\mRightarrow{} xs \mleq{} ys\} supposing strong-subtype(A;B)
Date html generated:
2017_04_17-AM-09_00_06
Last ObjectModification:
2017_02_27-PM-05_15_33
Theory : list_1
Home
Index