Step * 1 of Lemma fpf-sub_weakening


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


Latex:


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


Latex:
xxx(Unfold  `fpf-sub`  0  THEN  Auto)xxx




Home Index