proposition: Lemma le_eq_lt x y : le x y -> (x = y) + (lt x y).
proof: Proof. induction 1. destruct x. left; constructor. right; constructor. constructor. dependent elimination IHle as [inl id_refl|inr Hlt]. left; constructor. right; now constructor. Defined.
imports: Equations.Type.Loader Equations.Type.Relation Equations.Type.WellFounded