proposition: Lemma mk_list_app: forall n acc, mk_list_true_acc n acc = mk_list_true_acc n [] ++ acc.
proof: Proof. intro n. induction n as [ | n IHn]. + auto. + intro acc. simpl in *. rewrite IHn. cut (mk_list_true_acc n [] ++ [true] = mk_list_true_acc n [true]). intro H. rewrite <- H. rewrite <- app_assoc. unfold app. reflexivity. rewrite <- IHn. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance