proposition: Lemma S2_iff : forall n h h' s s', S2 n (hcons h s) (hcons h' s') <-> R2 n h h' /\ s = s' \/ h = h' /\ S2 n s s'.
proof: Proof. split. - inversion 1. + subst s; auto. + right;auto. - intros [[H0 H1] | [H0 H1]]. + subst s; now left. + subst h'; now right. 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)