---

Step * of Lemma decide2_wf

∀[T1,T2,T3,T4,T5:Type]. ∀[x:T1 + T2]. ∀[y:T3 + T4]. ∀[ll:T1 ⟶ T3 ⟶ T5]. ∀[lr:T1 ⟶ T4 ⟶ T5]. ∀[rl:T2 ⟶ T3 ⟶ T5].
∀[rr:T2 ⟶ T4 ⟶ T5].
  (case x,y
   of inl(a),inl(b) => ll[a;b]
    | inl(a),inr(b) => lr[a;b]
    | inr(a),inl(b) => rl[a;b]
    | inr(a),inr(b) => rr[a;b] ∈ T5)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T1,T2,T3,T4,T5:Type].  \mforall{}[x:T1  +  T2].  \mforall{}[y:T3  +  T4].  \mforall{}[ll:T1  {}\mrightarrow{}  T3  {}\mrightarrow{}  T5].  \mforall{}[lr:T1  {}\mrightarrow{}  T4  {}\mrightarrow{}  T5].
\mforall{}[rl:T2  {}\mrightarrow{}  T3  {}\mrightarrow{}  T5].  \mforall{}[rr:T2  {}\mrightarrow{}  T4  {}\mrightarrow{}  T5].
    (case  x,y
      of  inl(a),inl(b)  =>  ll[a;b]
        |  inl(a),inr(b)  =>  lr[a;b]
        |  inr(a),inl(b)  =>  rl[a;b]
        |  inr(a),inr(b)  =>  rr[a;b]  \mmember{}  T5)


By

---

Latex:
ProveWfLemma

---

Home Index