proposition: Theorem spec_double_size: forall x, [double_size x] = [x].
proof: Proof. intros x. rewrite double_size_fold. destr_t x as (n,x). rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_0. auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen