`∀[a,B:Top].  (let x,y = a in if a is a pair then B[a] otherwise 2 ~ let x,y = a in B[<x, y>])`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` ispair: `if z is a pair then a otherwise b` spread: spread def pair: `<a, b>` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ`
Lemmas referenced :  top_wf equal_wf has-value_wf_base is-exception_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis sqequalAxiom extract_by_obid sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache voidElimination voidEquality lambdaFormation sqequalSqle divergentSqle callbyvalueSpread productEquality productElimination sqleReflexivity equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination spreadExceptionCases axiomSqleEquality exceptionSqequal baseApply closedConclusion baseClosed

Latex:
\mforall{}[a,B:Top].    (let  x,y  =  a  in  if  a  is  a  pair  then  B[a]  otherwise  2  \msim{}  let  x,y  =  a  in  B[<x,  y>])

Date html generated: 2017_04_14-AM-07_35_21
Last ObjectModification: 2017_02_27-PM-03_08_12

Theory : fun_1

Home Index