proposition: Lemma BV_full_adder_carry_sym : forall (v w : BV) (cin : bool), BV_full_adder_carry v w cin = BV_full_adder_carry w v cin.
proof: Proof. simple induction v. simple induction w. auto. intros. rewrite BV_full_adder_carry_eq2. rewrite BV_full_adder_carry_eq3. rewrite H; auto. simple induction w. intros. rewrite BV_full_adder_carry_eq2. rewrite BV_full_adder_carry_eq3. rewrite H. auto. intros. do 2 rewrite BV_full_adder_carry_eq4. rewrite H. rewrite full_adder_carry_sym1. auto. Qed.
imports: BV FullAdder