proposition: Lemma form_ind : forall f, P f.
proof: Proof. intro f. remember (depth f) as n. revert f Heqn. induction n using Wf_nat.lt_wf_ind. destruct n. - destruct f ; simpl; auto; try discriminate. - destruct f; simpl ; try discriminate; intros. + apply PLOP; intros. apply (H (depth (elt x))); auto. inv Heqn. apply in_max_elt; auto. + intros. apply PLIMP; intros. * apply (H (depth (elt x))); auto. inv Heqn. apply in_max_elt with (Depth:= depth) in H0. lia. * apply (H (depth (elt t0))); auto. inv Heqn. lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause