---

Step * of Lemma destructor-product

No Annotations
∀[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.let x,y = p 
                       in let c1,L1 = pf x 
                          in let c2,L2 = pg y 
                             in <λL.<c1 firstn(||L1||;L), c2 nth_tl(||L1||;L)>, L1 @ L2>⌝⋅
   THEN All (Unfold `destructor`)
   THEN (MemTypeCD THENA 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 GenConclAtAddr [2;1]) }

1
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. T : {T:Type| T ⊆r Base} 
4. f : x:F[T] ⟶ decomp{i:l}(T.F[T];T;x)
5. g : x:G[T] ⟶ decomp{i:l}(T.G[T];T;x)
6. p1 : F[T]
7. p2 : G[T]
8. con : Constr(T.F[T])
9. v1 : {L:T List| ap-con(con;L) = p1 ∈ F[T]} 
10. v : decomp{i:l}(T.G[T];T;p2)
11. (g p2) = v ∈ decomp{i:l}(T.G[T];T;p2)
⊢ let c2,L2 = v 
  in <λL.<con firstn(||v1||;L), c2 nth_tl(||v1||;L)>, v1 @ L2> ∈ decomp{i:l}(T.F[T] × G[T];T;<p1, p2>)

---

Latex:

---

Latex:
No  Annotations
\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]  \mtimes{}  G[T]))


By

---

Latex:
(Auto
  THEN  RenameVar  `pf'  (-2)
  THEN  RenameVar  `pg'  (-1)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}p.let  x,y  =  p 
                                          in  let  c1,L1  =  pf  x 
                                                in  let  c2,L2  =  pg  y 
                                                      in  <\mlambda{}L.<c1  firstn(||L1||;L),  c2  nth\_tl(||L1||;L)>,  L1  @  L2>\mkleeneclose{}\mcdot{}
  THEN  All  (Unfold  `destructor`)
  THEN  (MemTypeCD  THENA  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  GenConclAtAddr  [2;1])

---

Home Index