proposition: Lemma in_max_elt : forall l x (IN: In x l), (Depth (elt x) < S(max_list l))%nat.
proof: Proof. induction l; simpl ; auto. - tauto. - intros. destruct IN ; simpl; auto. subst. lia. apply IHl in H. lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause