proposition: Lemma iota_compare_commute alpha beta: compare alpha beta = compare (iota_ij alpha) (iota_ij beta).
proof: Proof. reflexivity. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)