blob: a57b3bbad5b88dbe9ea5551ed54f88ce8f49bd00 (
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
30
31
32
33
34
35
36
37
38
39
40
41
|
1 subgoal
very_very_long_type_name1 : Type
very_very_long_type_name2 : Type
f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
============================
True
→ True
→ ∀ (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
1 subgoal
very_very_long_type_name1 : Type
very_very_long_type_name2 : Type
f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
============================
True
→ True
→ ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1)
(z : very_very_long_type_name2), f y x ∧ f y z
1 subgoal
very_very_long_type_name1 : Type
very_very_long_type_name2 : Type
f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
============================
True
→ True
→ ∀ (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
1 subgoal
very_very_long_type_name1 : Type
very_very_long_type_name2 : Type
f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
============================
True
→ True
→ ∃ (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
|
