---

Step * of Lemma free-from-atom-Knd

∀[a:Atom1]. ∀[k:Knd].  a#k:Knd
BY
{ ((Unfold `Knd` 0 THEN Auto) THEN D -1) }

1
1. a : Atom1
2. x : IdLnk × Id
⊢ a#inl x:IdLnk × Id + Id

2
1. a : Atom1
2. y : Id
⊢ a#inr y :IdLnk × Id + Id

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[k:Knd].    a\#k:Knd


By

---

Latex:
((Unfold  `Knd`  0  THEN  Auto)  THEN  D  -1)

---

Home Index