proposition: Lemma add_list_empty_l: forall (a: list bool), (add_list [] a) = [].
proof: Proof. intro a. induction a as [ | a xs IHxs]. - unfold add_list. simpl. reflexivity. - apply IHxs. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance