proposition: Lemma S1_app n : forall s1 s2 s3, S1 n s2 s3 -> S1 n (hy_app s1 s2) (hy_app s1 s3).
proof: Proof. induction s1; simpl hy_app. - trivial. - intros s2 s3 H; 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)