possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
(*<*)
theory Library
imports
BigO
Continuity
EfficientNat
ExecutableSet
ExecutableRat
FuncSet
Multiset
NatPair
Nat_Infinity
Nested_Environment
OptionalSugar
Permutation
Primes
Quotient
While_Combinator
Word
Zorn
Char_ord
Commutative_Ring
Coinductive_List
AssocList
begin
end
(*>*)