---

Step * 2 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#y:Y[x]
BY
{ Subst ⌜y ~ snd(<x, y>)⌝ 0⋅
THEN Try (Reduce 0⋅ THEN Complete (Auto))
THEN FreeFromAtomApElimType ⌜{p:x:X × Y[x]| (fst(p)) = x ∈ 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\#y:Y[x]


By

---

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

---

Home Index