∀(x : A) → B → x