proposition: Lemma R2_app n : forall s1 s2 , R2 n (node s1) (node s2) -> forall l, R2 n (node (hy_app l s1)) (node (hy_app l s2)).
proof: Proof. intros s1 s2 H; inversion H. - intros; constructor. apply S1_app; auto. - constructor 2; now apply S2_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)