---

Step * 1 of Lemma name_eq-normalize


1. G : Base
2. F : Base
3. b : Base
4. a : Base
5. ∃z:Base. (name_eq(a;b) ~ inl z)
⊢ F ~ F
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  G  :  Base
2.  F  :  Base
3.  b  :  Base
4.  a  :  Base
5.  \mexists{}z:Base.  (name\_eq(a;b)  \msim{}  inl  z)
\mvdash{}  F  \msim{}  F


By

---

Latex:
TACTIC:Auto

---

Home Index