---

Step * 1 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. 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])
BY
{ 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{}  \mlambda{}L.<ap-con(con;firstn(||v1||;L)),  ap-con(c1;nth\_tl(||v1||;L))>  \mmember{}  Constr(T.F[T]  \mtimes{}  G[T])


By

---

Latex:
Auto

---

Home Index