proposition: Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln.
proof: Proof. red_t; reflexivity. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen