Error with proposition on Optional data.

Stream: general

[Tamas Hadhazy]

def noInputCycleTest (nodes : Array (Option NodeTest)) : Prop :=
  ∀ oX ∈ nodes, ∀ oB ∈ nodes,
    match oX, oB with
    | some x, some b =>
      ∀ refB, b.ref = some refB → refB ∈ x.inputs → ¬ (match x.ref with | some r => r ∈ b.inputs | none => False)
    | _, _ => True

failed to synthesize
  Membership NodeRef (Array (Option NodeRef))

Hint: Additional diagnostic information

 may be available using the `set_option diagnostics true`

image.png
What might be wrong here?