---

Step * of Lemma one_or_both_ind_wf

∀[X:𝕌{j}]. ∀[A,B:Type]. ∀[x:one_or_both(A;B)]. ∀[both:bval:(A × B) ⟶ X]. ∀[left:lval:A ⟶ X]. ∀[right:rval:B ⟶ X].
  (one_or_both_ind(x;bval.both[bval];lval.left[lval];rval.right[rval]) ∈ X)
BY
{ DatatypeIndWf 2 `one_or_both` `one_or_both_ind`  }

---

Latex:

---

Latex:
\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[A,B:Type].  \mforall{}[x:one\_or\_both(A;B)].  \mforall{}[both:bval:(A  \mtimes{}  B)  {}\mrightarrow{}  X].  \mforall{}[left:lval:A  {}\mrightarrow{}  X].
\mforall{}[right:rval:B  {}\mrightarrow{}  X].
    (one\_or\_both\_ind(x;bval.both[bval];lval.left[lval];rval.right[rval])  \mmember{}  X)


By

---

Latex:
DatatypeIndWf  2  `one\_or\_both`  `one\_or\_both\_ind` 

---

Home Index