proposition: Theorem lub_unicity : forall P l l', lub P l -> lub P l' -> l = l'.
proof: Proof. intros P l l' (H1,(H2,H3)) (H'1,(H'2,H'3)). tricho l l' H4; trivial. - absurd (l t2< l). apply lt_irr. apply lt_le_trans with l';auto with T2. - absurd (l' t2< l'). apply lt_irr. apply lt_le_trans with l;auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)