Congruence Closure graph is not complete

[fxdpntthm]

def ctx4 : Ctx Term := [
  .type (#2 ~[★]~ #3), -- b ~ b'
  .type (#3 ~[★]~  (#5 `@k #1)), -- v ~ Maybe b'
  .type (#3 ~[★]~  (#4 `@k #1)), -- u ~ Maybe b
  .kind ★, -- b'
  .kind ★, -- b
  .kind ★, -- v
  .kind ★, -- u
  .datatype (★ -k> ★) -- Maybe 
  ]

#eval synth_coercion ctx4 #5 #6 -- u ~ v

Returns:

none

Expected output

.some (#2 `; (refl! [★ -> ★] #7) `@c #0  `; sym! #1)