---

Step * of Lemma fpf-val-single1

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,P:Top].  (z != x : v(x) ==> P[a;z] ~ True ⇒ P[x;v])
BY
{ xxx(((UnivCD THENA Auto)
       THEN RepUR ``fpf-val fpf-single fpf-dom`` 0
       THEN EqCD
       THEN Try (Trivial)
       THEN OldAutoBoolCase ⌜eq x x⌝⋅)
      THENA Auto
      )xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[x:A].  \mforall{}[v,P:Top].    (z  !=  x  :  v(x)  ==>  P[a;z]  \msim{}  True  {}\mRightarrow{}  P[x;v])


By

---

Latex:
xxx(((UnivCD  THENA  Auto)
          THEN  RepUR  ``fpf-val  fpf-single  fpf-dom``  0
          THEN  EqCD
          THEN  Try  (Trivial)
          THEN  OldAutoBoolCase  \mkleeneopen{}eq  x  x\mkleeneclose{}\mcdot{})
        THENA  Auto
        )xxx

---

Home Index