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. absurd (l < l). apply lt_irr. apply lt_le_trans with l';auto with T2. auto with T2. absurd (l' < l'). apply lt_irr. apply lt_le_trans with l;auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo