Goal:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  H : False
  ============================
   (tree_rec (Node Empty None Empty) = node Empty empty None Empty empty)


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