blob: 3c7c945ed8d3948ddb0d456fe8092fac70c13927 (
plain)
1
2
3
4
5
6
7
|
Require Import Coq.Arith.PeanoNat.
Hint Extern 1 => admit : typeclass_instances.
Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
intros a b f H.
rewrite H. (* Toplevel input, characters 15-25:
Anomaly: Evar ?X11 was not declared. Please report. *)
Abort.
|
