proposition: Lemma add_list_twice: forall a, add_list a a = removelast (false :: a).
proof: Proof. intro a. unfold add_list. rewrite add_list_carry_twice. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance