constructor
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
case mp
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

case mpr
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0