---

Step * 1 of Lemma record_extensionality


1. T : Atom ⟶ 𝕌'
2. r1 : record(x.T[x])
3. r2 : record(x.T[x])
4. ∀a:Atom. (r1.a = r2.a ∈ T[a])
⊢ r1 = r2 ∈ record(x.T[x])
BY
{ (All (Unfold `record`) THEN Ext THEN Auto THEN Fold `record-select` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Atom  {}\mrightarrow{}  \mBbbU{}'
2.  r1  :  record(x.T[x])
3.  r2  :  record(x.T[x])
4.  \mforall{}a:Atom.  (r1.a  =  r2.a)
\mvdash{}  r1  =  r2


By

---

Latex:
(All  (Unfold  `record`)  THEN  Ext  THEN  Auto  THEN  Fold  `record-select`  0  THEN  Auto)

---

Home Index