Goal:
  
  ============================
   (forall (A : Type) (v : A) (p : positive),
    set p v Empty =
    match p with
    | xI q => Node Empty None (set q v Empty)
    | xO q => Node (set q v Empty) None Empty
    | xH => Node Empty (Some v) Empty
    end)


DEBUG:Going to execute:
destruct p

Goals:
    A : Type  v : A  p : positive
  ============================
   (set (xI p) v Empty = Node Empty None (set p v Empty))

    A : Type  v : A  p : positive
  ============================
   (set (xO p) v Empty = Node (set p v Empty) None Empty)

    A : Type  v : A
  ============================
   (set xH v Empty = Node Empty (Some v) Empty)


DEBUG:Going to execute:
reflexivity

Goals:
    A : Type  v : A  p : positive
  ============================
   (set (xI p) v Empty = Node Empty None (set p v Empty))

    A : Type  v : A  p : positive
  ============================
   (set (xO p) v Empty = Node (set p v Empty) None Empty)

    A : Type  v : A
  ============================
   (set xH v Empty = Node Empty (Some v) Empty)


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