Nuprl Lemma : fun_thru_spread
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C,D:Type]. ∀[f:C ⟶ D]. ∀[b:x:A ⟶ B[x] ⟶ C].
((f let x,y = p in b[x;y]) = let x,y = p in f b[x;y] ∈ D)
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
so_apply: x[s],
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2]
Rules used in proof :
Error :functionIsType,
Error :universeIsType,
hypothesisEquality,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
applyEquality,
functionEquality,
because_Cache,
Error :inhabitedIsType,
universeEquality,
Error :productIsType,
productEquality,
cumulativity,
Error :isect_memberFormation_alt,
introduction,
cut,
hypothesis,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
axiomEquality,
productElimination
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[p:x:A \mtimes{} B[x]]. \mforall{}[C,D:Type]. \mforall{}[f:C {}\mrightarrow{} D]. \mforall{}[b:x:A {}\mrightarrow{} B[x] {}\mrightarrow{} C].
((f let x,y = p in b[x;y]) = let x,y = p in f b[x;y])
Date html generated:
2019_06_20-AM-11_17_58
Last ObjectModification:
2018_09_26-AM-10_25_09
Theory : core_2
Home
Index