proposition: Lemma BV_full_adder_sum_eq4 : forall (vh : bool) (vt : list bool) (wh : bool) (wt : list bool) (b : bool), BV_full_adder_sum (vh :: vt) (wh :: wt) b = consbv (full_adder_sum vh wh b) (BV_full_adder_sum vt wt (full_adder_carry vh wh b)).
proof: Proof. auto. Qed.
imports: BV FullAdder