---

Step * 1 of Lemma uiff_inversion


1. [P] : ℙ
2. [Q] : ℙ
3. uiff(Q;P)@i
⊢ uiff(P;Q)
BY
{ (D (-1) THEN D 0 THEN D 0 THEN Try (Complete (Auto)) THEN OnMaybeHyp 4 (\h. (D h THEN Complete (Auto)))) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  uiff(Q;P)@i
\mvdash{}  uiff(P;Q)


By

---

Latex:
(D  (-1)
  THEN  D  0
  THEN  D  0
  THEN  Try  (Complete  (Auto))
  THEN  OnMaybeHyp  4  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))

---

Home Index