---

Step * 1 of Lemma is-atomic_wf


1. x : Base
2. (x)↓
⊢ if x is a pair then ff otherwise if x is inl then ff
                                   else if x is inr then ff
                                        else tt ∈ 𝔹
BY
{ ((BLemma `ispair-member` THEN Auto) THEN (BLemma `isinl-member` THEN Auto) THEN BLemma `isinr-member`⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Base
2.  (x)\mdownarrow{}
\mvdash{}  if  x  is  a  pair  then  ff  otherwise  if  x  is  inl  then  ff
                                                                      else  if  x  is  inr  then  ff
                                                                                else  tt  \mmember{}  \mBbbB{}


By

---

Latex:
((BLemma  `ispair-member`  THEN  Auto)
  THEN  (BLemma  `isinl-member`  THEN  Auto)
  THEN  BLemma  `isinr-member`\mcdot{}
  THEN  Auto)

---

Home Index