`∀[x,y,F:Top].  (name_eq(let a,b = x in F[a;b];y) ~ let a,b = x in name_eq(F[a;b];y))`

Proof

Definitions occuring in Statement :  name_eq: `name_eq(x;y)` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` spread: spread def sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_apply: `x[s1;s2]` name_eq: `name_eq(x;y)` name-deq: `NameDeq` list-deq: `list-deq(eq)` all: `∀x:A. B[x]` top: `Top` eq_atom: `x =a y` band: `p ∧b q` bfalse: `ff` list_ind: list_ind it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` null: `null(as)` strict4: `strict4(F)` and: `P ∧ Q` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` or: `P ∨ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]`
Lemmas referenced :  atomdeq_reduce_lemma istype-void lifting-strict-atom_eq strict4-decide lifting-strict-callbyvalue strict4-apply lifting-strict-spread has-value_wf_base istype-base is-exception_wf lifting-strict-ispair lifting-strict-isaxiom strictness-apply istype-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution dependent_functionElimination thin Error :isect_memberEquality_alt,  voidElimination hypothesis isectElimination baseClosed independent_isectElimination independent_pairFormation Error :lambdaFormation_alt,  callbyvalueCallbyvalue callbyvalueReduce Error :universeIsType,  baseApply closedConclusion hypothesisEquality callbyvalueExceptionCases Error :inrFormation_alt,  imageMemberEquality imageElimination exceptionSqequal Error :inlFormation_alt,  axiomSqEquality Error :inhabitedIsType,  Error :isectIsTypeImplies

Latex:
\mforall{}[x,y,F:Top].    (name\_eq(let  a,b  =  x  in  F[a;b];y)  \msim{}  let  a,b  =  x  in  name\_eq(F[a;b];y))

Date html generated: 2019_06_20-PM-01_58_03
Last ObjectModification: 2019_01_29-AM-09_26_25

Theory : decidable!equality

Home Index