blob: 36efc42d478e9d8f0148483691330c755dba4c5d (
plain)
1
2
3
4
5
6
|
Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')),
@eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b)))
(p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))).
Proof.
intros.
Fail generalize dependent (a, b).
|
