- { 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 _ )
+ { pentagon : forall a b c d, (assoc a _ _ ) >>>
+ (assoc _ _ _ ) ~~
+ (second _ _ a (assoc b c d )) >>>
+ (assoc _ _ _ ) >>>
+ (first _ _ _ (assoc a b _ ))