---

Step * of Lemma test-evd1

∀[A,B,C,D,E:ℙ].  ((((A ∧ B) ⇒ (A ∧ B)) ⇒ (C ∨ D)) ⇒ (C ⇒ E) ⇒ (D ⇒ E) ⇒ E)
BY
{ (EvidenceTac ⌜λh,f,g. (case h (λx.x) of inl(a) => f | inr(b) => g 
                         case h (λp.let x,y = p in <x, y>) of inl(c) => c | inr(d) => d)⌝⋅
   THENA Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D,E:\mBbbP{}].    ((((A  \mwedge{}  B)  {}\mRightarrow{}  (A  \mwedge{}  B))  {}\mRightarrow{}  (C  \mvee{}  D))  {}\mRightarrow{}  (C  {}\mRightarrow{}  E)  {}\mRightarrow{}  (D  {}\mRightarrow{}  E)  {}\mRightarrow{}  E)


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}h,f,g.  (case  h  (\mlambda{}x.x)  of  inl(a)  =>  f  |  inr(b)  =>  g 
                                              case  h  (\mlambda{}p.let  x,y  =  p  in  <x,  y>)  of  inl(c)  =>  c  |  inr(d)  =>  d)\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index