proposition: Lemma strict_lub_unique : forall s l l', strict_lub s l -> strict_lub s l' -> l = l'.
proof: Proof. intros s l l' H H'; destruct H, H'; apply LE_antisym;eauto. apply H0. auto with T1. intro; apply LE_r; auto. apply H2. intro; apply LE_r; auto. 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)