proposition: Lemma BV_full_adder_sum_v_nil_false : forall v : BV, BV_full_adder_sum v nilbv false = v.
proof: Proof. unfold nilbv in |- *. simple induction v. trivial. intros. rewrite BV_full_adder_sum_eq3. rewrite half_adder_carry_false. rewrite half_adder_sum_false. rewrite H; auto. Qed.
imports: BV FullAdder