- { pentagon : forall a b c d, (assoc a _ _ ) >>>
- (assoc _ _ _ ) ~~
- (second _ _ a (assoc b c d )) >>>
- (assoc _ _ _ ) >>>
- (first _ _ _ (assoc a b _ ))
+ { pentagon : forall a b c d, (first _ _ d (assoc a b c )) >>>
+ (assoc a _ d ) >>>
+ (second _ _ a (assoc b c d ))
+ ~~ (assoc _ c d ) >>>
+ (assoc a b _ )