blob: 35db82bd4c57daa52bea0a7c73e3c859c30e7f05 (
plain)
1
2
3
4
5
6
7
8
|
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.
|
