def Apply.oapply {n m n' m' : ℕ} (op : Bool → Bool → Bool) (O : OBdd n m) (U : OBdd n' m') : (s : ℕ) × { OU : OBdd (max n n') s // ∀ (I : Vector Bool (max n n')), OU.evaluate I = op (O.evaluate (Vector.cast ⋯ (I.take n))) (U.evaluate (Vector.cast ⋯ (I.take n'))) }

Equations

• One or more equations did not get rendered due to their size.