proposition: Lemma has_form_mono : isMono has_form.
proof: Proof. unfold isMono. intros. revert Fm. remember (elt x) as f. revert x Heqf. induction f using form_ind; intros. - destruct x; simpl in * ; try congruence. subst. inv Fm. constructor ; auto. - destruct x; simpl in * ; try congruence. subst. inv Fm. eapply wf_OP; eauto. rewrite Forall_forall in *. intros. specialize (H4 x H0). eapply H ; eauto. - destruct x; simpl in * ; try congruence. subst. inv Fm. eapply wf_IMPL;eauto. rewrite Forall_forall in *. intros. specialize (H4 x H0). eapply H ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause