proposition: Lemma compare_of_phi0 alpha beta: compare (phi0 alpha) (phi0 beta) = compare alpha beta.
proof: Proof. cbn; now destruct (compare alpha beta). Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)