proposition: Remark R30 : gamma <> zero -> gamma = beta.
proof: Proof. case_eq l. - intro; assert False by (apply R29;auto); contradiction. - intros n0 H H0; apply R27;auto. rewrite H;auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)