proposition: Lemma scalL_wf: forall l x sc, wfe x -> wft sc -> wfe (fst (scalL sc x l)) /\ wft (snd (scalL sc x l)).
proof: Proof. intros l1; elim l1; simpl; auto. intros a l2 Hrec x sc H1 H2. generalize (scal_wf a _ H1 H2); case scal; simpl. intros a1 sc1 (H3, H4); auto. generalize (scal_list_wf l2 _ H1 H4); case scal_list; simpl. intros a2 sc2; case a2; simpl; auto. intros x1 y1 z1 ((V1, (V2, V3)), V4); apply Hrec; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod