Nuprl Lemma : ap-con_wf
∀[F:Type ⟶ Type]. ∀[T:{T:Type| T ⊆r Base} ]. ∀[con:Constr(T.F[T])]. ∀[L:T List]. (ap-con(con;L) ∈ F[T])
Proof
Definitions occuring in Statement :
ap-con: ap-con(con;L),
constructor: Constr(T.F[T]),
list: T List,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
base: Base,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
ap-con: ap-con(con;L),
member: t ∈ T,
constructor: Constr(T.F[T]),
subtype_rel: A ⊆r B,
so_apply: x[s],
so_lambda: λ2x.t[x]
Lemmas referenced :
subtype_rel_wf,
base_wf,
list_wf,
constructor_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
applyEquality,
cut,
sqequalRule,
lambdaEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
hypothesis,
isectEquality,
setEquality,
universeEquality,
cumulativity,
lemma_by_obid,
thin,
functionEquality,
setElimination,
rename
Latex:
\mforall{}[F:Type {}\mrightarrow{} Type]. \mforall{}[T:\{T:Type| T \msubseteq{}r Base\} ]. \mforall{}[con:Constr(T.F[T])]. \mforall{}[L:T List].
(ap-con(con;L) \mmember{} F[T])
Date html generated:
2016_05_15-PM-06_55_49
Last ObjectModification:
2015_12_27-AM-11_40_11
Theory : general
Home
Index