proposition: Lemma length_sextend: forall a i, length (sextend a i) = ((length a) + i)%nat.
proof: Proof. intros. unfold sextend. case_eq a. intros. rewrite length_mk_list_false. easy. intros. apply length_extend. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance