fact: Fixpoint standard_gnaw (i:nat)(alpha : T1)(l:nat): T1 := match l with | 0 => alpha | S m => standard_gnaw (S i) (canon alpha i) m end.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)