---

Step * 2 of Lemma assert-hasloc


1. i : Id
2. x3 : Id
3. x4 : Id × Id
4. x2 : Id
5. (fst(x4)) = i ∈ Id supposing True
⊢ ¬¬((fst(x4)) = i ∈ Id)
BY
{ ((D 0 THEN Auto) THEN D -2 THEN Auto) }

---

Latex:



1.  i  :  Id
2.  x3  :  Id
3.  x4  :  Id  \mtimes{}  Id
4.  x2  :  Id
5.  (fst(x4))  =  i  supposing  True
\mvdash{}  \mneg{}\mneg{}((fst(x4))  =  i)


By

((D  0  THEN  Auto)  THEN  D  -2  THEN  Auto)

---

Home Index