proposition: Lemma length_mk_list_true: forall n, length (mk_list_true n) = n.
proof: Proof. intro n. induction n as [ | n' IHn]. - simpl. auto. - simpl. apply f_equal. exact IHn. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance