proposition: Lemma largeSb_b (alpha : T1) (s: list nat) : largeSb alpha s = largeb alpha (shift s).
proof: Proof. induction s;cbn. - unfold largeb, largeSb; now rewrite gnaw_gnawS. - cbn; unfold largeb, largeSb; cbn; intros; now rewrite gnaw_gnawS, shift_unshift. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)