The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/24/2014 02:38 PM, Jason Gross wrote:
> proof_admitted is just a proof of [False] that is used to implement the
> [admit] tactic.  You can only use it to get around "Instance is not
> well-typed" when your instance came from [admit]; in this case, you're
> essentially just running [admit] again.

Ok - doing this more better:

Goal exists n, n=0.
refine (ex_intro _ _ _).
assert  {m:nat|m=0} as H by (eexists;reflexivity).
destruct H as [x H].
exact x.

Makes the remaining goal:

  ============================
   (fun H : {m : nat | m = 0} => let (x, _) := H in x)
     (exist (fun m : nat => m = 0) 0 eq_refl) = 0

Which is solvable by reflexivity (because hnf or cbv beta iota makes it 
0=0).

Interesting...

Can one transform an existing evar into such a thing?  Or only those 
introduced by refine?

-- Jonathan