Step
*
of Lemma
req-rat2real
No Annotations
∀q1,q2:ℚ. uiff(rat2real(q1) = rat2real(q2);q1 = q2 ∈ ℚ)
BY
{ Auto }
1
1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
⊢ q1 = q2 ∈ ℚ
Latex:
Latex:
No Annotations
\mforall{}q1,q2:\mBbbQ{}. uiff(rat2real(q1) = rat2real(q2);q1 = q2)
By
Latex:
Auto
Home
Index