proposition: Lemma S2_app : forall n s1 s2 , S2 n s1 s2 -> forall l, S2 n (hy_app l s1) (hy_app l s2).
proof: Proof. intros n s1 s2 h; eapply S2_ind2 with (P := fun h1 h2 _ => match h1, h2 with node s1, node s2 => forall l, R2 n (node (hy_app l s1)) (node (hy_app l s2)) end). - intros; constructor. apply S1_app; auto. intros; eauto. - constructor 2. induction l. + cbn; auto. + cbn; now constructor 2. - intros h0 h' s r H l; destruct h0, h'; induction l. + simpl;auto. + simpl;auto; constructor 2;auto. - auto. - eexact h. 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)