---

Step * 1 of Lemma fun_thru_spread


1. A : Type
2. B : A ⟶ Type
3. p : x:A × B[x]
4. C : Type
5. D : Type
6. f : C ⟶ D
7. b : x:A ⟶ B[x] ⟶ C
⊢ (f let x,y = p in b[x;y]) = let x,y = p in f b[x;y] ∈ D
BY
{ (New [`x';`y'] (D 3) THEN AbReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  p  :  x:A  \mtimes{}  B[x]
4.  C  :  Type
5.  D  :  Type
6.  f  :  C  {}\mrightarrow{}  D
7.  b  :  x:A  {}\mrightarrow{}  B[x]  {}\mrightarrow{}  C
\mvdash{}  (f  let  x,y  =  p  in  b[x;y])  =  let  x,y  =  p  in  f  b[x;y]


By

---

Latex:
(New  [`x';`y']  (D  3)  THEN  AbReduce  0  THEN  Auto)

---

Home Index