---

Step * of Lemma band-wf-partial

∀[a:partial(Base)]. ∀[b:partial(𝔹)].  (a ∧b b ∈ partial(𝔹))
BY
{ TACTIC:(RepUR ``band ifthenelse`` 0 THEN (UnivCD ⋅ THENA Auto)) }

1
1. a : partial(Base)
2. b : partial(𝔹)
⊢ case a of inl() => b | inr() => ff ∈ partial(𝔹)

---

Latex:

---

Latex:
\mforall{}[a:partial(Base)].  \mforall{}[b:partial(\mBbbB{})].    (a  \mwedge{}\msubb{}  b  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
TACTIC:(RepUR  ``band  ifthenelse``  0  THEN  (UnivCD  \mcdot{}  THENA  Auto))

---

Home Index