proposition: Lemma R1_app : forall s1 s2 s3, R1 (node s2) (node s3) -> R1 (node (hy_app s1 s2)) (node (hy_app s1 s3)).
proof: Proof. constructor; inversion H; now apply S0_app. 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)