---

Step * 1 1 of Lemma all_functionality_wrt_uiff


1. S : Type
2. T : Type
3. P : S ⟶ ℙ
4. Q : T ⟶ ℙ
5. S = T ∈ Type
6. p : ∀x:T. uiff(P[x];Q[x])
7. x : T
8. P x
⊢ fst((p x)) ∈ Q x
BY
{ (RenameVar `q' (-1)
   THEN GenConclAtAddr [2;1]
   THEN D -2
   THEN Reduce 0
   THEN With ⌜q⌝ (DVar `v1') ⋅
   THEN RepUR ``so_apply`` -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  P  :  S  {}\mrightarrow{}  \mBbbP{}
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
5.  S  =  T
6.  p  :  \mforall{}x:T.  uiff(P[x];Q[x])
7.  x  :  T
8.  P  x
\mvdash{}  fst((p  x))  \mmember{}  Q  x


By

---

Latex:
(RenameVar  `q'  (-1)
  THEN  GenConclAtAddr  [2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  With  \mkleeneopen{}q\mkleeneclose{}  (DVar  `v1')  \mcdot{}
  THEN  RepUR  ``so\_apply``  -1
  THEN  Auto)

---

Home Index