## Stream: new members

#### Claus-Peter Becke (Sep 09 2020 at 08:32):

variables (men : Type*) (barber : men)
variable (shaves : men → men → Prop)

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : false :=
begin
end


It is to prove that a contradiction follows from the hypotheses. My goal is to find two hypotheses which contradict each other. The first I would like to do is to remove the universal quantifier from the hypothesis. To be able to do that, x should be introduced. But to introduce it as an arbitrary object presupposes that the quantified x appears inside the goal. The only way to achieve this is to use the revert-tactic as far as I see. But after having done that I'll get an implication forall x ... -> false. Which alternatives do I have?

#### Kenny Lau (Sep 09 2020 at 08:32):

have h1 := h barber

@Kenny Lau
Thanks.

#### Alexandre Rademaker (Sep 10 2020 at 00:16):

why using Type* ? Why not only Type?

#### Scott Morrison (Sep 10 2020 at 00:20):

Don't you have barbers in your universe? :-)

#### Alexandre Rademaker (Sep 10 2020 at 01:00):

Sorry, I didn't understand.

#### Kenny Lau (Sep 10 2020 at 06:10):

Type* means in an arbitrary universe