---

Step * 2 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)
⊢ a ~ b
BY
{ TACTIC:(InstLemma `sq-decider-name-deq` []⋅ THEN BackThruHyp' (-1) THEN 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{}  a  \msim{}  b


By

---

Latex:
TACTIC:(InstLemma  `sq-decider-name-deq`  []\mcdot{}  THEN  BackThruHyp'  (-1)  THEN  Auto)

---

Home Index