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