Goal:
  
  x : V.t
  s0 : VSet.t
  s1 : VSet.t
  s2 : VSet.t
  disjadd : DisjointAdd x s1 s2
  disj20 : Disjoint s2 s0
  ============================
   (Disjoint s1 s0)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrapply@0> $1

Goals:
  
  x : V.t
  s0 : VSet.t
  s1 : VSet.t
  s2 : VSet.t
  disjadd : DisjointAdd x s1 s2
  disj20 : Disjoint s2 s0
  ============================
   (DisjointAdd ?Goal0 s1 ?Goal1)

  
  x : V.t
  s0 : VSet.t
  s1 : VSet.t
  s2 : VSet.t
  disjadd : DisjointAdd x s1 s2
  disj20 : Disjoint s2 s0
  ============================
   (Disjoint ?Goal1 s0)


DEBUG:Going to execute:
eassumption
DEBUG LTAC Evaluated term: (Disjoint_DisjointAdd ?t ?t0 ?t1 ?t2 ?d ?d0)

Goals:
  
  x : V.t
  s0 : VSet.t
  s1 : VSet.t
  s2 : VSet.t
  disjadd : DisjointAdd x s1 s2
  disj20 : Disjoint s2 s0
  ============================
   (DisjointAdd ?Goal0 s1 ?Goal1)

  
  x : V.t
  s0 : VSet.t
  s1 : VSet.t
  s2 : VSet.t
  disjadd : DisjointAdd x s1 s2
  disj20 : Disjoint s2 s0
  ============================
   (Disjoint ?Goal1 s0)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::eassumption@0>