---

Step * of Lemma fpf-union-compatible_wf

∀[A,C:Type]. ∀[B:A ─→ Type].
  ∀[eq:EqDecider(A)]. ∀[f,g:x:A fp-> B[x] List]. ∀[R:(C List) ─→ C ─→ 𝔹].
    (fpf-union-compatible(A;C;x.B[x];eq;R;f;g) ∈ ℙ) 
  supposing ∀x:A. (B[x] ⊆r C)
BY
{ (Auto
   THEN Unfold `fpf-union-compatible` 0
   THEN All (Unfold `so_apply`)
   THEN Auto
   THEN Try ((DoSubsume THEN Auto THEN SubtypeReasoning THEN Auto))) }

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:x:A  fp->  B[x]  List].  \mforall{}[R:(C  List)  {}\mrightarrow{}  C  {}\mrightarrow{}  \mBbbB{}].
        (fpf-union-compatible(A;C;x.B[x];eq;R;f;g)  \mmember{}  \mBbbP{}) 
    supposing  \mforall{}x:A.  (B[x]  \msubseteq{}r  C)


By

(Auto
  THEN  Unfold  `fpf-union-compatible`  0
  THEN  All  (Unfold  `so\_apply`)
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto  THEN  SubtypeReasoning  THEN  Auto)))

---

Home Index