proposition: Lemma length_extend: forall a i b, length (extend a i b) = ((length a) + i)%nat.
proof: Proof. intro a. induction a. - intros. simpl. now rewrite extend_size_zero. - intros. induction i. + intros. simpl. lia. + intros. simpl. apply f_equal. rewrite IHi. simpl. lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance