proposition: Lemma R2_iff i s s' : R2 i (node s) (node s') <-> S1 i s s' \/ S2 i s s'.
proof: Proof. split. - inversion 1; auto. - destruct 1; [left| right];trivial. 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)