proposition: Lemma mk_list_false_equiv: forall t acc, mk_list_false_acc t acc = (List.rev (mk_list_false t)) ++ acc.
proof: Proof. induction t as [ |t IHt]; auto; intro acc; simpl; rewrite IHt. rewrite app_assoc_reverse. apply f_equal. simpl. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance