---

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
{ (((UnivCD THENA Auto)
    THEN RepUR ``fpf-val fpf-single fpf-dom`` 0
    THEN EqCD
    THEN Try (Trivial)
    THEN OldAutoBoolCase ⌈eq x x⌉⋅)
   THENA Auto
   ) }

---

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

(((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
  )

---

Home Index