---

Step * of Lemma test-model2

∀[Dom:Type]. ∀[A,B:Dom ⟶ ℙ].
  ((∀x:Dom. ∃y:Dom. (A[y] ∨ B[y]))
  ⇒ (∀x,y,z:Dom.  ((A[y] ∧ A[z]) ⇒ A[x]))
  ⇒ (∀x,y,z:Dom.  ((B[y] ∧ B[z]) ⇒ A[x]))
  ⇒ (∀x:Dom. A[x]))
BY
{ (EvidenceTac ⌜λf,g,h,x. let y,AorB = f x 
                          in case AorB
                              of inl(A) =>
                              let y1,aORb = (λz.f) 33 x 
                              in case aORb of inl(a) => g x y y1 <A, a> | inr(b) => Y (λx.x)
                              | inr(B) =>
                              let y1,aORb = hd([f]) x 
                              in case aORb of inl(a) => Y (λx.x) | inr(b) => h x y y1 <B, b>⌝⋅
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[Dom:Type].  \mforall{}[A,B:Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Dom.  \mexists{}y:Dom.  (A[y]  \mvee{}  B[y]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((A[y]  \mwedge{}  A[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((B[y]  \mwedge{}  B[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  A[x]))


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}f,g,h,x.  let  y,AorB  =  f  x 
                                                in  case  AorB
                                                        of  inl(A)  =>
                                                        let  y1,aORb  =  (\mlambda{}z.f)  33  x 
                                                        in  case  aORb  of  inl(a)  =>  g  x  y  y1  <A,  a>  |  inr(b)  =>  Y  (\mlambda{}x.x)
                                                        |  inr(B)  =>
                                                        let  y1,aORb  =  hd([f])  x 
                                                        in  case  aORb  of  inl(a)  =>  Y  (\mlambda{}x.x)  |  inr(b)  =>  h  x  y  y1  <B,  b>\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index