cases assign output
  <;> cases assign lhs
    <;> cases assign rhs
      <;> cases linv
        <;> cases rinv
          <;> decide
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
no goals