discriminate

discriminate

Coq < Goal 1 = 2 -> False.
1 subgoal
  
  ============================
   1 = 2 -> False

Unnamed_thm < intro.
1 subgoal
  
  H : 1 = 2
  ============================
   False

Unnamed_thm < discriminate.
Proof completed.