proposition: Lemma BV_full_adder_sum_eq3 : forall (vh : bool) (vt : list bool) (b : bool), BV_full_adder_sum (vh :: vt) nil b = consbv (half_adder_sum vh b) (BV_full_adder_sum vt nil (half_adder_carry vh b)).
proof: Proof. auto. Qed.
imports: BV FullAdder