Nuprl Lemma : spread-spread

[t:Top × Top]. ∀[P,Q:Top].  (let x,y let a,b in P[a;b] in Q[x;y] let a,b in let x,y P[a;b] in Q[x;y])


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] spread: spread def product: x:A × B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule sqequalAxiom hypothesis because_Cache sqequalHypSubstitution isect_memberEquality isectElimination hypothesisEquality lemma_by_obid productEquality

Latex:
\mforall{}[t:Top  \mtimes{}  Top].  \mforall{}[P,Q:Top].
    (let  x,y  =  let  a,b  =  t 
                          in  P[a;b] 
      in  Q[x;y]  \msim{}  let  a,b  =  t 
                              in  let  x,y  =  P[a;b] 
                                    in  Q[x;y])



Date html generated: 2018_05_21-PM-00_01_26
Last ObjectModification: 2018_01_28-PM-02_24_27

Theory : union


Home Index