---

Step * of Lemma free-from-atom-pair

∀[a:Atom1]. ∀[X,Y:Type]. ∀[x:X]. ∀[y:Y].  (a#<x, y>:X × Y) supposing (a#y:Y and a#x:X)
BY
{ (Repeat ((D 0 THENA Complete (Auto)))
   THEN (InstLemma `free-from-atom_wf` [⌜Y⌝;⌜y⌝;⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `free-from-atom_wf` [⌜X⌝;⌜x⌝;⌜a⌝]⋅ THENA Auto)) }

1
1. a : Atom1
2. X : Type
3. Y : Type
4. x : X
5. y : Y
6. a#x:X
7. a#y:Y
8. a#y:Y ∈ ℙ
9. a#x:X ∈ ℙ
⊢ a#<x, y>:X × Y

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[X,Y:Type].  \mforall{}[x:X].  \mforall{}[y:Y].    (a\#<x,  y>:X  \mtimes{}  Y)  supposing  (a\#y:Y  and  a\#x:X)


By

---

Latex:
(Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  (InstLemma  `free-from-atom\_wf`  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `free-from-atom\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index