proposition: Lemma S0_app : forall s1 s2 s3, S0 s2 s3 -> S0 (hy_app s1 s2) (hy_app s1 s3).
proof: Proof. induction s1. - cbn; auto. - intros; cbn; constructor;auto. Qed.
imports: Coq(Arith Lia List Relation_Operators Operators_Properties Peano_dec Wellfounded.Inverse_Image Wellfounded.Inclusion) hydras(More_Arith Epsilon0 Hessenberg Simple_LexProd MoreLibHyps)