---

Step * 1 of Lemma destructor-product


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>)
BY
{ (Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN Unfold `decomp` 0
   THEN (Fold `ap-con` 0 THEN (MemCD THENA Auto))
   THEN RepUR ``ap-con`` 0
   THEN Fold `ap-con` 0) }

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. c1 : Constr(T.G[T])
11. v2 : {L:T List| ap-con(c1;L) = p2 ∈ G[T]} 
⊢ λL.<ap-con(con;firstn(||v1||;L)), ap-con(c1;nth_tl(||v1||;L))> ∈ Constr(T.F[T] × G[T])

2
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. c1 : Constr(T.G[T])
11. v2 : {L:T List| ap-con(c1;L) = p2 ∈ G[T]} 
⊢ v1 @ v2 ∈ {L:T List| <ap-con(con;firstn(||v1||;L)), ap-con(c1;nth_tl(||v1||;L))> = <p1, p2> ∈ (F[T] × G[T])} 

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  G  :  Type  {}\mrightarrow{}  Type
3.  T  :  \{T:Type|  T  \msubseteq{}r  Base\} 
4.  f  :  x:F[T]  {}\mrightarrow{}  decomp\{i:l\}(T.F[T];T;x)
5.  g  :  x:G[T]  {}\mrightarrow{}  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\} 
10.  v  :  decomp\{i:l\}(T.G[T];T;p2)
11.  (g  p2)  =  v
\mvdash{}  let  c2,L2  =  v 
    in  <\mlambda{}L.<con  firstn(||v1||;L),  c2  nth\_tl(||v1||;L)>,  v1  @  L2>  \mmember{}  decomp\{i:l\}(T.F[T]  \mtimes{}  G[T];T;<p1
                                                                                                                                                                                          ,  p2
                                                                                                                                                                                          >)


By

---

Latex:
(Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Unfold  `decomp`  0
  THEN  (Fold  `ap-con`  0  THEN  (MemCD  THENA  Auto))
  THEN  RepUR  ``ap-con``  0
  THEN  Fold  `ap-con`  0)

---

Home Index