proposition: Lemma extend_size_one: forall i a b, length (extend [a] i b) = S i.
proof: Proof. intros. induction i. - now simpl. - simpl. now rewrite IHi. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance