blob: b9413a4ac2a846b138b6110daa9ff680317245f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* Set Printing Existential Instances. *)
Unset Solve Unification Constraints.
Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
Goal True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier.
refine (nat_rect _ _ _ _).
Show.
Admitted.
Set Printing Existential Instances.
Goal forall n m : nat, True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier.
intros.
refine (nat_rect _ _ _ _).
Show.
clear n.
Show.
3:clear m.
Show.
Admitted.
|
