---

Step * of Lemma destructor-sum

∀[F,G:Type ⟶ Type].  (destructor{i:l}(T.F[T]) ⇒ destructor{i:l}(T.G[T]) ⇒ destructor{i:l}(T.F[T] + G[T]))
BY
{ (Auto
   THEN RenameVar `pf' (-2)
   THEN RenameVar `pg' (-1)
   THEN UseWitness ⌜λp.case p
                        of inl(x) =>
                        let c,L = pf x 
                        in <λL.(inl (c L)), L>
                        | inr(x) =>
                        let c,L = pg x 
                        in <λL.(inr (c L) ), L>⌝⋅
   THEN (All (Unfold `destructor`)
         THEN MemTypeCD
         THEN Try (Complete (Auto))
         THEN (GenConcl ⌜pf = f ∈ (x:F[T] ⟶ decomp{i:l}(T.F[T];T;x))⌝⋅ THENA Auto)
         THEN (GenConcl ⌜pg = g ∈ (x:G[T] ⟶ decomp{i:l}(T.G[T];T;x))⌝⋅ THENA Auto)
         THEN ThinVar `pg'
         THEN ThinVar `pf'
         THEN (MemCD THENA Auto)
         THEN (D -1
               THEN Reduce 0
               THEN GenConclAtAddr [2;1]
               THEN Thin (-1)
               THEN D -1
               THEN Reduce 0
               THEN (Unfold `decomp` 0
                     THEN Auto
                     THEN Fold `ap-con` 0
                     THEN Auto
                     THEN (MemTypeCD THEN Auto THEN (RepUR ``ap-con`` 0 THEN Auto THEN Fold `ap-con` 0 THEN Auto)⋅)⋅)⋅)
         ⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (destructor\{i:l\}(T.F[T])  {}\mRightarrow{}  destructor\{i:l\}(T.G[T])  {}\mRightarrow{}  destructor\{i:l\}(T.F[T]  +  G[T]))


By

---

Latex:
(Auto
  THEN  RenameVar  `pf'  (-2)
  THEN  RenameVar  `pg'  (-1)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}p.case  p
                                            of  inl(x)  =>
                                            let  c,L  =  pf  x 
                                            in  <\mlambda{}L.(inl  (c  L)),  L>
                                            |  inr(x)  =>
                                            let  c,L  =  pg  x 
                                            in  <\mlambda{}L.(inr  (c  L)  ),  L>\mkleeneclose{}\mcdot{}
  THEN  (All  (Unfold  `destructor`)
              THEN  MemTypeCD
              THEN  Try  (Complete  (Auto))
              THEN  (GenConcl  \mkleeneopen{}pf  =  f\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (GenConcl  \mkleeneopen{}pg  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ThinVar  `pg'
              THEN  ThinVar  `pf'
              THEN  (MemCD  THENA  Auto)
              THEN  (D  -1
                          THEN  Reduce  0
                          THEN  GenConclAtAddr  [2;1]
                          THEN  Thin  (-1)
                          THEN  D  -1
                          THEN  Reduce  0
                          THEN  (Unfold  `decomp`  0
                                      THEN  Auto
                                      THEN  Fold  `ap-con`  0
                                      THEN  Auto
                                      THEN  (MemTypeCD
                                                  THEN  Auto
                                                  THEN  (RepUR  ``ap-con``  0  THEN  Auto  THEN  Fold  `ap-con`  0  THEN  Auto)\mcdot{})\mcdot{})\mcdot{})\mcdot{})
  \mcdot{})

---

Home Index