---

Step * of Lemma fpf-sub-val2

∀[A,A':Type].
  ∀[B:A ⟶ Type]
    ∀eq:EqDecider(A'). ∀f,g:a:A fp-> B[a]. ∀x:A'.
      ∀[P,Q:a:A ⟶ B[a] ⟶ ℙ].
        ((∀x:A. ∀z:B[x].  (P[x;z] ⇒ Q[x;z])) ⇒ z != f(x) ==> P[x;z] ⇒ z != g(x) ==> Q[x;z] supposing g ⊆ f) 
  supposing strong-subtype(A;A')
BY
{ Repeat ((D 0 THENA Complete (Auto))) }

1
1. [A] : Type
2. [A'] : Type
3. strong-subtype(A;A')
4. [B] : A ⟶ Type
5. eq : EqDecider(A')@i
6. f : a:A fp-> B[a]@i
7. g : a:A fp-> B[a]@i
8. x : A'@i
9. [P] : a:A ⟶ B[a] ⟶ ℙ
10. [Q] : a:A ⟶ B[a] ⟶ ℙ
11. ∀x:A. ∀z:B[x].  (P[x;z] ⇒ Q[x;z])@i
12. g ⊆ f
⊢ z != f(x) ==> P[x;z] ⇒ z != g(x) ==> Q[x;z]

---

Latex:

---

Latex:
\mforall{}[A,A':Type].
    \mforall{}[B:A  {}\mrightarrow{}  Type]
        \mforall{}eq:EqDecider(A').  \mforall{}f,g:a:A  fp->  B[a].  \mforall{}x:A'.
            \mforall{}[P,Q:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}].
                ((\mforall{}x:A.  \mforall{}z:B[x].    (P[x;z]  {}\mRightarrow{}  Q[x;z]))
                {}\mRightarrow{}  z  !=  f(x)  ==>  P[x;z]  {}\mRightarrow{}  z  !=  g(x)  ==>  Q[x;z]  supposing  g  \msubseteq{}  f) 
    supposing  strong-subtype(A;A')


By

---

Latex:
Repeat  ((D  0  THENA  Complete  (Auto)))

---

Home Index