Coq < Coq < 1 goal
  
  ============================
  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

x < 
x < 1 focused goal
(shelved: 1)
  i : nat
  ============================
  exists k : nat, i = ?j /\ ?j = k /\ i = k

(fun i : nat =>
 ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)

x < 1 focused goal
(shelved: 2)
  i : nat
  ============================
  i = ?j /\ ?j = ?k /\ i = ?k

(fun i : nat =>
 ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
   ?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))

x < 2 focused goals
(shelved: 2)
  i : nat
  ============================
  i = ?j

goal 2 is:
 ?j = ?k /\ i = ?k

(fun i : nat =>
 ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
   ?j
   (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) 
      ?k (conj ?Goal ?Goal0)))

x <