∀[q:ℚ]. ((q/1) = q ∈ ℚ)
{ Auto }
1. q : ℚ
⊢ (q/1) = q ∈ ℚ