---

Step * 1 1 of Lemma random_wf


1. p : FinProbSpace
2. a : Atom2
3. b : Atom2
⊢ random(p;a;b) = random(p;a;b) ∈ (ℕ ─→ Outcome)
BY
{ (Refine `randomEquality` []  THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  a  :  Atom2
3.  b  :  Atom2
\mvdash{}  random(p;a;b)  =  random(p;a;b)


By

(Refine  `randomEquality`  []    THEN  Auto)

---

Home Index