blob: 9fee61fb74356a2fbf2bf5b482c4ccdc5faa5b38 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Check that untypable beta-expansion are trapped *)
Variable A:nat->Type.
Variable n:nat.
Variable P : (m:nat)m=n->Prop.
Goal (p:n=n)(P n p).
Intro.
Pattern n p. (* Non typable generalization *)
|