---

Step * of Lemma decide_wf

∀[T1,T2,T3:Type]. ∀[x:T1 + T2]. ∀[l:T1 ⟶ T3]. ∀[r:T2 ⟶ T3].  (case x of inl(a) => l[a] | inr(b) => r[b] ∈ T3)
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
\mforall{}[T1,T2,T3:Type].  \mforall{}[x:T1  +  T2].  \mforall{}[l:T1  {}\mrightarrow{}  T3].  \mforall{}[r:T2  {}\mrightarrow{}  T3].
    (case  x  of  inl(a)  =>  l[a]  |  inr(b)  =>  r[b]  \mmember{}  T3)


By

---

Latex:
TACTIC:Auto

---

Home Index