---

Step * 1 of Lemma fpf-sub_weakening


1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. g : a:A fp-> B[a]
⊢ g ⊆ g
BY
{ (Unfold `fpf-sub` 0 THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)
4.  g  :  a:A  fp->  B[a]
\mvdash{}  g  \msubseteq{}  g


By

(Unfold  `fpf-sub`  0  THEN  Auto)

---

Home Index