---

Step * of Lemma free-from-atom-pair-iff

∀[a:Atom1]. ∀[X:Type]. ∀[Y:𝕌']. ∀[x:X]. ∀[y:Y].  uiff(a#<x, y>:x:X × Y;a#x:X ∧ a#y:Y)
BY
{ ((At ⌜𝕌{i''}⌝ (UniformUnivCD Auto)⋅ THENA Auto)
   THEN At ⌜𝕌{i''}⌝ (Auto)⋅
   THEN Try ((FLemma `free-from-atom-pair-components` [6] THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[X:Type].  \mforall{}[Y:\mBbbU{}'].  \mforall{}[x:X].  \mforall{}[y:Y].    uiff(a\#<x,  y>:x:X  \mtimes{}  Y;a\#x:X  \mwedge{}  a\#y:Y)


By

---

Latex:
((At  \mkleeneopen{}\mBbbU{}\{i''\}\mkleeneclose{}  (UniformUnivCD  Auto)\mcdot{}  THENA  Auto)
  THEN  At  \mkleeneopen{}\mBbbU{}\{i''\}\mkleeneclose{}  (Auto)\mcdot{}
  THEN  Try  ((FLemma  `free-from-atom-pair-components`  [6]  THEN  Auto)))

---

Home Index