### Nuprl Lemma : record+_extensionality

`∀[T:Atom ⟶ 𝕌']. ∀[B:record(x.T[x]) ⟶ 𝕌']. ∀[z:Atom]. ∀[r1,r2:record(x.T[x])`
`                                                               z:B[self]].`
`  uiff(r1 = r2 ∈ record(x.T[x])z:B[self];(r1 = r2 ∈ record(x.T[x])) ∧ (r1.z = r2.z ∈ B[r1]))`

Proof

Definitions occuring in Statement :  record-select: `r.x` record+: record+ record: `record(x.T[x])` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` and: `P ∧ Q` function: `x:A ⟶ B[x]` atom: `Atom` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` record+: record+ uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` record-select: `r.x` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` nequal: `a ≠ b ∈ T ` not: `¬A` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` top: `Top`
Lemmas referenced :  record+_wf istype-atom record_wf istype-universe subtype_rel-equal eq_atom_wf eqtt_to_assert assert_of_eq_atom top_wf eqff_to_assert atom_subtype_base bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot neg_assert_of_eq_atom equal_wf equal-wf-base assert_wf bnot_wf not_wf istype-assert istype-void uiff_transitivity iff_transitivity iff_weakening_uiff assert_of_bnot record-select_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution independent_pairFormation sqequalRule productElimination thin independent_pairEquality axiomEquality hypothesis isect_memberEquality_alt isectElimination hypothesisEquality isectIsTypeImplies inhabitedIsType universeIsType because_Cache extract_by_obid lambdaEquality_alt applyEquality functionIsType instantiate universeEquality dependentIntersectionEqElimination applyLambdaEquality lambdaFormation_alt unionElimination equalityElimination independent_isectElimination cumulativity equalityIsType1 equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination dependent_pairFormation_alt equalityIsType4 baseApply closedConclusion baseClosed promote_hyp voidElimination dependentIntersection_memberEquality dependentIntersectionElimination functionExtensionality_alt atomEquality productIsType

Latex:
\mforall{}[T:Atom  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[B:record(x.T[x])  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[z:Atom].  \mforall{}[r1,r2:record(x.T[x])
z:B[self]].
uiff(r1  =  r2;(r1  =  r2)  \mwedge{}  (r1.z  =  r2.z))

Date html generated: 2019_10_15-AM-11_28_58
Last ObjectModification: 2018_10_16-PM-02_30_02

Theory : general

Home Index