---

Step * 1 of Lemma isect2-record


1. T1 : Atom ⟶ Type
2. T2 : Atom ⟶ Type
⊢ record(x.T1[x]) ⋂ record(x.T2[x]) ⊆r record(x.T1[x] ⋂ T2[x])
BY
{ (Unfold `record` 0
   THEN D 0
   THEN Auto
   THEN Isect2HD (-1)
   THEN ExtWith [`z'] [⌜x:Atom ⟶ T1[x]⌝]⋅
   THEN Try (Complete (Auto))
   THEN Isect2CD
   THEN Try (Complete (Auto))
   THEN Thin (-2)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T1  :  Atom  {}\mrightarrow{}  Type
2.  T2  :  Atom  {}\mrightarrow{}  Type
\mvdash{}  record(x.T1[x])  \mcap{}  record(x.T2[x])  \msubseteq{}r  record(x.T1[x]  \mcap{}  T2[x])


By

---

Latex:
(Unfold  `record`  0
  THEN  D  0
  THEN  Auto
  THEN  Isect2HD  (-1)
  THEN  ExtWith  [`z']  [\mkleeneopen{}x:Atom  {}\mrightarrow{}  T1[x]\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Isect2CD
  THEN  Try  (Complete  (Auto))
  THEN  Thin  (-2)
  THEN  Auto)

---

Home Index