proposition: Lemma iota_mono : forall alpha beta, lt alpha beta <-> lt (iota_ij alpha) (iota_ij beta).
proof: Proof. split; unfold lt; cbn; auto. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)