---

Step * 1 2 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. 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])} 
BY
{ (((MemTypeCD THENW Auto) THENM Auto)
   THEN (EqCD THEN Auto)
   THEN (Subst' firstn(||v1||;v1 @ v2) ~ v1 0 THENM Auto)
   THEN (RWO "firstn_append" 0 THENA (Auto THEN Auto'))
   THEN RWO "firstn_all" 0
   THEN Auto) }

---

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.  c1  :  Constr(T.G[T])
11.  v2  :  \{L:T  List|  ap-con(c1;L)  =  p2\} 
\mvdash{}  v1  @  v2  \mmember{}  \{L:T  List|  <ap-con(con;firstn(||v1||;L)),  ap-con(c1;nth\_tl(||v1||;L))>  =  <p1,  p2>\} 


By

---

Latex:
(((MemTypeCD  THENW  Auto)  THENM  Auto)
  THEN  (EqCD  THEN  Auto)
  THEN  (Subst'  firstn(||v1||;v1  @  v2)  \msim{}  v1  0  THENM  Auto)
  THEN  (RWO  "firstn\_append"  0  THENA  (Auto  THEN  Auto'))
  THEN  RWO  "firstn\_all"  0
  THEN  Auto)

---

Home Index