---

Step * of Lemma record_extensionality

∀[T:Atom ⟶ 𝕌']. ∀[r1,r2:record(x.T[x])].  uiff(r1 = r2 ∈ record(x.T[x]);∀a:Atom. (r1.a = r2.a ∈ T[a]))
BY
{ Auto }

1
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])

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index