Unfolding.v

Require Import Coq.Program.Program.
Require Import Coq.Lists.List.

Axiom ignore_termination: nat.

Program Fixpoint id (l: list nat) { measure ignore_termination } :=
  match l with
  | nil => nil
  | x :: xs => x :: id xs
  end.

Admit Obligations.

Parameter x: nat.
Parameter l: list nat.
Parameter r: list nat.

(* false goal *)
Goal id (x :: l) = r.
  unfold id.
  simpl. (* does nothing *)
  cbn. (* creates a huge term *)
  fold id. (* does nothing *)