theorem evalFin_eq_eval (t : Term) (vars : ℕ → BitStream) : (t.evalFin fun (i : Fin t.arity) => vars ↑i) = t.eval vars

theorem eq_iff_xor_eq_zero (seq₁ : BitStream) (seq₂ : BitStream) : (∀ (i : ℕ), seq₁ i = seq₂ i) ↔ ∀ (i : ℕ), (seq₁ ^^^ seq₂) i = BitStream.zero i

theorem eval_eq_iff_xor_eq_zero (t₁ : Term) (t₂ : Term) : t₁.eval = t₂.eval ↔ (t₁.xor t₂).evalFin = fun (x : Fin (t₁.xor t₂).arity → BitStream) => BitStream.zero