`∀[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