---

Step * of Lemma if-per-void

∀[t:Top]. (per-void() ⇒ t)
BY
{ (Intros
   THEN Unfold `per-void` (-1)
   THEN (Assert ⌜t = t ∈ pertype(λa,b. (tt ≤ ff))⌝⋅ THENA Auto)
   THEN UseWitness ⌜Ax⌝⋅
   THEN PerHD (-1)
   THEN InstLemma `not-btrue-sqle-bfalse` []
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[t:Top].  (per-void()  {}\mRightarrow{}  t)


By

---

Latex:
(Intros
  THEN  Unfold  `per-void`  (-1)
  THEN  (Assert  \mkleeneopen{}t  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  PerHD  (-1)
  THEN  InstLemma  `not-btrue-sqle-bfalse`  []
  THEN  Auto)

---

Home Index