Skip to content

Commit 81a2f44

Browse files
authored
Merge pull request #1955 from jdchristensen/join-associator
JoinAssoc: tiny fix to join_associator
2 parents 7c5ce31 + 7d07f4e commit 81a2f44

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

theories/Homotopy/Join/JoinAssoc.v

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -263,8 +263,7 @@ Defined.
263263
Global Instance join_associator : Associator Join.
264264
Proof.
265265
snrapply Build_Associator; simpl.
266-
- intros A B C.
267-
apply join_assoc.
266+
- exact join_assoc.
268267
- intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.
269268
apply join_assoc_nat.
270269
Defined.

0 commit comments

Comments
 (0)