proposition: Lemma double_size_level : forall x, level (double_size x) = S (level x).
proof: Proof. intros x. rewrite double_size_fold; unfold level at 2. destr_t x as (n,x). apply mk_t_S_level. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen