---

Step * of Lemma sq_stable__allowed

No Annotations
∀[T:𝕌']. ∀[x:Provisional(T)].  SqStable(allowed(x))
BY
{ (Auto THEN (D 0 THENA Auto) THEN UseWitness ⌜Ax⌝⋅ THEN D -1 THEN Unhide THEN D 2 THEN Fold `member` 0) }

1
1. T : 𝕌'
2. x : Base
3. x1 : Base
4. x = x1 ∈ (x,y:ok:ℙ × T supposing ok//((fst(x) ⇐⇒ fst(y)) ∧ ((fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T))))
5. x ∈ ok:ℙ × T supposing ok
6. x1 ∈ ok:ℙ × T supposing ok
7. (fst(x) ⇐⇒ fst(x1)) ∧ ((fst(x)) ⇒ ((snd(x)) = (snd(x1)) ∈ T))
8. allowed(x)
⊢ Ax ∈ allowed(x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  \mforall{}[x:Provisional(T)].    SqStable(allowed(x))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  D  -1
  THEN  Unhide
  THEN  D  2
  THEN  Fold  `member`  0)

---

Home Index