blob: 312eed8309515cf523eacee6077d3cf519d7fe1c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool eqtype fintype ssrnat.
Variable T : Type.
Lemma test0 : forall a b c d : T, True.
Proof. by move=> a b {a} a c; exact I. Qed.
Variable P : T -> Prop.
Lemma test1 : forall a b c : T, P a -> forall d : T, True.
Proof. move=> a b {a} a _ d; exact I. Qed.
Definition Q := forall x y : nat, x = y.
Axiom L : 0 = 0 -> Q.
Axiom L' : 0 = 0 -> forall x y : nat, x = y.
Lemma test3 : Q.
by apply/L.
Undo.
rewrite /Q.
by apply/L.
Undo 2.
by apply/L'.
Qed.
|
