Goal:
  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   False


DEBUG:Going to execute:
elim id
Level 2: evaluation returns
<coq-core.plugins.tauto::is_disj@0>
where
tauto_flags := 
of type
tauto_flags
X1 := V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
of type
constr of type tacvalue


Goals:
  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   (V.lt x x -> False)

  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   (V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y -> False)


DEBUG:Going to execute:
intro
DEBUG LTAC Evaluated term: H

Goals:
  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   (V.lt x x -> False)

  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   (V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y -> False)


DEBUG:Going to execute:
<coq-core.plugins.ltac::intro@0>

Goals:
  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  H0 : V.lt x x
  ============================
   False

  
  x : V.t
  n : Z
  y : V.t
  H : V.lt x x \/ V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  H0 : V.eq x x /\ n < n \/ V.eq x x /\ n = n /\ V.lt y y
  ============================
   False


DEBUG:Going to execute:
clear id