---

Step * 1 of Lemma free-from-atom-pair-components


1. a : Atom1
2. X : Type
3. Y : X ⟶ 𝕌'
4. x : X
5. y : Y[x]
6. a#<x, y>:x:X × Y[x]
⊢ a#x:X
BY
{ Subst ⌜x ~ fst(<x, y>)⌝ 0⋅
THEN Try (Reduce 0⋅ THEN Complete (Auto))
THEN FreeFromAtomApElimType ⌜x:X × Y[x]⌝ ⌜<x, y>⌝⋅
THEN Auto }

---

Latex:

---

Latex:

1.  a  :  Atom1
2.  X  :  Type
3.  Y  :  X  {}\mrightarrow{}  \mBbbU{}'
4.  x  :  X
5.  y  :  Y[x]
6.  a\#<x,  y>:x:X  \mtimes{}  Y[x]
\mvdash{}  a\#x:X


By

---

Latex:
Subst  \mkleeneopen{}x  \msim{}  fst(<x,  y>)\mkleeneclose{}  0\mcdot{}
THEN  Try  (Reduce  0\mcdot{}  THEN  Complete  (Auto))
THEN  FreeFromAtomApElimType  \mkleeneopen{}x:X  \mtimes{}  Y[x]\mkleeneclose{}  \mkleeneopen{}<x,  y>\mkleeneclose{}\mcdot{}
THEN  Auto

---

Home Index