blob: 42b07e5a08918188e35835191693f3c2e77fd80c (
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
|
Require Import Coq.Unicode.Utf8.
Section test.
Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type).
Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop).
Lemma test : True -> True ->
forall (x : very_very_long_type_name1) (y : very_very_long_type_name2),
f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
Proof. Show. Abort.
Lemma test : True -> True ->
forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
(z : very_very_long_type_name2),
f y x /\ f y z.
Proof. Show. Abort.
Lemma test : True -> True ->
forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
(z : very_very_long_type_name2),
f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z.
Proof. Show. Abort.
Lemma test : True -> True ->
exists (x : very_very_long_type_name1) (y : very_very_long_type_name2),
f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
Proof. Show. Abort.
End test.
|
