---

Step * 1 of Lemma fpf-empty-join


1. A : Type
2. B : A ─→ Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
5. eq : EqDecider(A)
⊢ (λa.if a ∈b d) then f1 a else ⋅ fi ) = f1 ∈ (a:{a:A| (a ∈ d)}  ─→ B[a])
BY
{ (Ext
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Try (((Fold `member` 0 THEN MemCD) THENA Auto))
   THEN (D (-1))
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  d  :  A  List
4.  f1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a]
5.  eq  :  EqDecider(A)
\mvdash{}  (\mlambda{}a.if  a  \mmember{}\msubb{}  d)  then  f1  a  else  \mcdot{}  fi  )  =  f1


By

(Ext
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  (((Fold  `member`  0  THEN  MemCD)  THENA  Auto))
  THEN  (D  (-1))
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index