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.
|
