blob: 7869532c67a48e9884b308810587b48052eff6aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* coq-prog-args: ("-nois") *)
Inductive eq {A : Type} (x : A) : forall a:A, Prop := eq_refl : eq x x.
Axiom sym : forall A (x y : A) (_ : eq x y), eq y x.
Require Import Ltac.
Register eq as core.eq.type.
Register sym as core.eq.sym.
Goal forall A (x y:A) (_ : forall z, eq y z), eq x x.
intros * H. replace x with y.
- reflexivity.
- apply H.
Qed.
|
