blob: a27600957afad7d27e0f24d40c1ce2f0ab336a79 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import TestSuite.admit.
Require Import Coq.Arith.PeanoNat.
Hint Extern 1 => admit : typeclass_instances.
Require Import Setoid.
Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop),
Equivalence R -> R a b -> f a = f b.
intros a b f H.
intros. Fail rewrite H1.
Abort.
|
