---

Step * of Lemma test-hidden-ap

∀[A,B,C:Type].  (((A ⇒ A) ⇒ (B ∨ C)) ⇒ (C ⇒ B) ⇒ B)
BY
{ (EvidenceTac ⌜λf,g. let id = λx.x in
                       let ap1 = f id in
                       let F = case ap1 of inl(b) => f | inr(c) => f in
                       let Id = case ap1 of inl(b) => id | inr(c) => id in
                       case ap1 of inl(b) => case F Id of inl(b) => b | inr(c) => Y id | inr(c) => g c⌝⋅
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    (((A  {}\mRightarrow{}  A)  {}\mRightarrow{}  (B  \mvee{}  C))  {}\mRightarrow{}  (C  {}\mRightarrow{}  B)  {}\mRightarrow{}  B)


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}f,g.  let  id  =  \mlambda{}x.x  in
                                          let  ap1  =  f  id  in
                                          let  F  =  case  ap1  of  inl(b)  =>  f  |  inr(c)  =>  f  in
                                          let  Id  =  case  ap1  of  inl(b)  =>  id  |  inr(c)  =>  id  in
                                          case  ap1  of  inl(b)  =>  case  F  Id  of  inl(b)  =>  b  |  inr(c)  =>  Y  id  |  inr(c)  =>  g  c\000C\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index