Why does the example from "How to make ad hoc proof automation less ad hoc" fail with regular apply?

lessadhocapply.v

Set Implicit Arguments.
Unset Strict Implicit.

(*
The first example from the paper
"How to make ad hoc proof automation less ad hoc",
don't work as expected with the non-ssreflect apply.
 *)

(* The example works over separation logic heaps
but details are not needed so just declare
everything as axioms. *)
Parameters heap ptr : Type.
Parameters
  (elem : ptr -> forall [A:Type], A -> heap)
  (sep : heap -> heap -> heap)
  (def : heap -> Prop).
Parameters
  (def_left : forall h1 h2, def (sep h1 h2) -> def h1)
  (def_right : forall h1 h2, def (sep h1 h2) -> def h2).

(* Concretely define the goal predicate, to be more sure
   the part of the code building proofs is correct.
   [in_dom x h] stands for $x \elem dom h$ in the paper.
 *)
Inductive in_dom (x:ptr) : heap -> Prop :=
| in_here : forall [A] (v:A), in_dom x (elem x v)
| in_left : forall h1 h2, in_dom x h1 -> in_dom x (sep h1 h2)
| in_right : forall h1 h2, in_dom x h2 -> in_dom x (sep h1 h2).

(* Now all the canonical structure stuff, exactly following the paper *)
Structure tagged_heap := Tag {untag : heap}.
Definition right_tag h := Tag h.
Definition left_tag h := right_tag h.
Canonical found_tag h := left_tag h.

Definition spec x (h : tagged_heap)
  := def (untag h) -> in_dom x (untag h).
Structure find x := Find { heap_of : tagged_heap; _ : spec x heap_of }.

Lemma found_pf A x (v:A) : spec x (found_tag (elem x v)).
Proof.
  intro. apply in_here.
Qed.
Canonical found_struct A x (v:A) :=
  @Find x (found_tag (elem x v)) (@found_pf A x v).

Lemma left_pf x h (f:find x):
  spec x (left_tag (sep (untag (heap_of f)) h)).
Proof.
  destruct f as [hl sl].
  intros d%def_left.
  apply in_left, sl, d.
Qed.
Canonical left_struct x h (f : find x) :=
  @Find x (left_tag (sep (untag (heap_of f)) h)) (@left_pf x h f).

Lemma right_pf x h (f:find x):
  spec x (right_tag (sep h (untag (heap_of f)))).
Proof.
  destruct f as [hr sr].
  intros d%def_right.
  apply in_right, sr, d.
Qed.
Canonical right_struct x h (f : find x) :=
  @Find x (right_tag (sep h (untag (heap_of f)))) (@right_pf x h f).

Lemma indom (x:ptr) (f : find x):
  def (untag (heap_of f)) -> in_dom x (untag (heap_of f)).
Proof.
  destruct f as [? s]. apply s.
Qed.

Example ex1 A (x1 x2 : ptr) (v1 v2 : A) (h1 h2 : heap)
  (h:= sep h1 (sep (elem x1 1) (elem x2 3))):
  def h -> in_dom x2 h.
Proof.
  intro d.
  (* regular apply fails, saying <<Unable to unify "x1" with "x2".>> *)
  Fail apply indom.
  (* but ssreflect's apply: works *)
Require Import ssreflect.
  apply: indom.
  exact d.
Qed.