blob: 30e6d57a7ae7960faeb7eb3263ae0f0540f2560d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Set Universe Polymorphism.
Require Import ssreflect.
Axiom mult@{i} : nat -> nat -> nat.
Notation "m * n" := (mult m n).
Axiom multA : forall a b c, (a * b) * c = a * (b * c).
(* Previously the following gave a universe error: *)
Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)).
Proof. by rewrite !multA. Qed.
|
