Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *)
(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
Require Coq.Lists.List.

Import Coq.Lists.List.

Set Implicit Arguments.
Global Set Asymmetric Patterns.

Section machine.
  Variables pc state : Type.

  Inductive propX (i := pc) (j := state) : list Type -> Type :=
  | Inj : forall G, Prop -> propX G
  | ExistsX : forall G A, propX (A :: G) -> propX G.

  Implicit Arguments Inj [G].

  Definition PropX := propX nil.
  Fixpoint last (G : list Type) : Type.
    exact (match G with
             | nil => unit
             | T :: nil => T
             | _ :: G' => last G'
           end).
  Defined.
  Fixpoint eatLast (G : list Type) : list Type.
    exact (match G with
             | nil => nil
             | _ :: nil => nil
             | x :: G' => x :: eatLast G'
           end).
  Defined.

  Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
    match p with
      | Inj _ P => fun _ => Inj P
      | ExistsX G A p1 => fun p' =>
                            match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
                              | nil => fun p1 _ => ExistsX p1
                              | _ :: _ => fun _ rc => ExistsX rc
                            end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with
                                                | nil => fun _ _ => Inj True
                                                | _ => fun p' => p'
                                              end p'))
    end.

  Definition spec := state -> PropX.
  Definition codeSpec := pc -> option spec.

  Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P.
  Definition interp specs := valid specs nil.
End machine.
Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope.
Bind Scope PropX_scope with PropX propX.
Variables pc state : Type.

Inductive subs : list Type -> Type :=
| SNil : subs nil
| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts).

Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) :=
  match s in subs G return subs (T :: G) with
    | SNil => SCons _ nil f SNil
    | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f)
  end.

Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state :=
  match s in subs G return propX pc state G -> PropX pc state with
    | SNil => fun p => p
    | SCons _ _ f s' => fun p => Substs s' (subst p f)
  end.
Variable specs : codeSpec pc state.

Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)),
                               interp specs (Substs s (ExX  : A, p))
                               -> exists a, interp specs (Substs (SPush s a) p).
admit.
Defined.

Goal    forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G))
               (s : subs G)
               (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p)))
               (P : forall _ : subs (@cons Type A G), Prop)
               (_ : forall (s0 : subs (@cons Type A G))
                           (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)),
                      P s0),
          @ex (forall _ : A, PropX pc state)
              (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)).
  intros ? ? ? ? H ? H'.
  apply simplify_fwd_ExistsX in H.
  firstorder. 
Qed.
 (* Toplevel input, characters 15-19:
Error: Illegal application:
The term "cons" of type "forall A : Type, A -> list A -> list A"
cannot be applied to the terms
 "Type" : "Type"
 "T" : "Type"
 "G0" : "list Type"
The 2nd term has type "Type@{Top.53}" which should be coercible to
 "Type@{Top.12}".
 *)