---

Step * 1 of Lemma fpf-sub-val


1. [A] : Type
2. [B] : A ─→ Type
3. eq : EqDecider(A)@i
4. f : a:A fp-> B[a]@i
5. g : a:A fp-> B[a]@i
6. x : A@i
7. [P] : a:A ─→ B[a] ─→ ℙ
8. ∀x:A. ((↑x ∈ dom(g)) ⇒ ((↑x ∈ dom(f)) c∧ (g(x) = f(x) ∈ B[x])))
9. ↑x ∈ dom(g)@i
10. ↑x ∈ dom(f)
11. g(x) = f(x) ∈ B[x]
12. P[x;f(x)]@i
⊢ P[x;g(x)]
BY
{ ((HypSubst (-2) 0) THEN Auto) }

---

Latex:



1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)@i
4.  f  :  a:A  fp->  B[a]@i
5.  g  :  a:A  fp->  B[a]@i
6.  x  :  A@i
7.  [P]  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(g))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(f))  c\mwedge{}  (g(x)  =  f(x))))
9.  \muparrow{}x  \mmember{}  dom(g)@i
10.  \muparrow{}x  \mmember{}  dom(f)
11.  g(x)  =  f(x)
12.  P[x;f(x)]@i
\mvdash{}  P[x;g(x)]


By

((HypSubst  (-2)  0)  THEN  Auto)

---

Home Index