---

Step * of Lemma ispair-or-isaxiom-append-nil

∀l:Base. ((l @ [])↓ ⇒ ((↑ispair(l @ [])) ∨ (↑isaxiom(l @ []))))
BY
{ (Auto THEN HVimplies2 0 [1;1] THEN (OrRight THENA Auto) THEN HVimplies2 0 [1]) }

1
1. l : Base@i
2. (l @ [])↓@i
3. ∀a,b:Top.  (if l @ [] is a pair then a otherwise b ~ b)
4. ∀a,b:Top.  (if l @ [] = Ax then a otherwise b ~ b)
⊢ False

---

Latex:

---

Latex:
\mforall{}l:Base.  ((l  @  [])\mdownarrow{}  {}\mRightarrow{}  ((\muparrow{}ispair(l  @  []))  \mvee{}  (\muparrow{}isaxiom(l  @  []))))


By

---

Latex:
(Auto  THEN  HVimplies2  0  [1;1]  THEN  (OrRight  THENA  Auto)  THEN  HVimplies2  0  [1])

---

Home Index