aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/programequality.v
blob: 414c572f81f1d25aa600285d6cfcde584426ef2e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Require Import Program.

Axiom t : nat -> Set.

Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type)
       (a : t x),
    P (eq_rect _ _ a _ e) e'.
Proof.
  intros.
  pi_eq_proofs. clear e.
  destruct e'. simpl.
  change (P a eq_refl).
Abort.