---

Step * of Lemma test-model3

∀[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 y1,y1AorB = f x 
                          in let y2,y2AorB = (λz.f) 33 x 
                             in case y1AorB
                                 of inl(A) =>
                                 case y2AorB of inl(a) => g x y1 y2 <A, a> | inr(b) => Y (λx.x)
                                 | inr(B) =>
                                 case y2AorB of inl(a) => Y (λx.x) | inr(b) => h x y1 y2 <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  y1,y1AorB  =  f  x 
                                                in  let  y2,y2AorB  =  (\mlambda{}z.f)  33  x 
                                                      in  case  y1AorB
                                                              of  inl(A)  =>
                                                              case  y2AorB  of  inl(a)  =>  g  x  y1  y2  <A,  a>  |  inr(b)  =>  Y  (\mlambda{}x.x)
                                                              |  inr(B)  =>
                                                              case  y2AorB  of  inl(a)  =>  Y  (\mlambda{}x.x)  |  inr(b)  =>  h  x  y1  y2  <B,  b>\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index