Inductive id : Type :=
  | Id : nat -> id.

Definition beq_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 => beq_nat n1 n2
  end.

Theorem beq_id_refl : forall x, true = beq_id x x.
Proof.
  intros.
  destruct x.
  simpl.
  apply beq_nat_refl.
Qed.

Module PartialMap.
Export NatList.

Inductive partial_map : Type :=
  | empty  : partial_map
  | record : id -> nat -> partial_map -> partial_map.

Fixpoint update (d : partial_map)
                  (x : id) (value : nat)
                  : partial_map :=
  match d with
  | empty => record x value empty
  | record i n xs => match beq_id x i with
                         | true  => record i value xs
                         | false => record i n (update xs x value)
                    end
  end.

Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty         => None
  | record y v d' => if beq_id x y
                     then Some v
                     else find x d'
  end.

Theorem update_eq :
  forall (d : partial_map) (x : id) (v: nat),
    find x (update d x v) = Some v.
Proof.
  intros.
  simpl.
  induction d.
  - simpl.
    rewrite <- beq_id_refl.
    reflexivity.
  - simpl.
    case (beq_id x i).
    + simpl.
    (* if beq_id x i then Some v else find x d *)
Qed.