proposition: Lemma chkHc_has_form : forall m f i b, chkHc m f i b = true -> has_form m (HCons.mk i b f).
proof: Proof. intros m f i. revert i. induction f using form_ind. - simpl. intros. destruct (@IntMap.get' _ KInt _ i m) eqn:EQ; try congruence. destruct p as (b',f). destruct f ; try congruence. rewrite! andb_true_iff in H. rewrite! eqb_true_iff in H. destruct H as ((H1, H2),H3). subst. assert (a = i0) by lia ; subst. econstructor ; eauto. - simpl ; intros. repeat rewrite andb_true_iff in H0. destruct H0 as (ALL & GET). destruct (@IntMap.get' _ KInt _ i m)eqn:FIND; try congruence. destruct p as (b',f). destruct f ; intuition try congruence. rewrite! andb_true_iff in GET. destruct GET as (((EQOP & ALLDEC) & EQB) & CHECK). rewrite eqb_true_iff in *. subst. apply lop_eqb_true in EQOP. subst. apply wf_OP with (l:= l) in FIND;auto. + rewrite forallb_forall in ALL. rewrite Forall_forall. intros. specialize (H _ H0 _ _ (ALL _ H0)). destruct x; auto. - simpl ; intros. repeat rewrite andb_true_iff in H0. destruct H0 as ((ALL1 & ALL2) & GET). destruct (@IntMap.get' _ KInt _ i m)eqn:FIND; try congruence. destruct p as (b',f). destruct f ; intuition try congruence. rewrite! andb_true_iff in GET. destruct GET as (((EQOP & ALLDEC) & EQB) & CHECK). rewrite eqb_true_iff in *. subst. apply wf_IMPL with (l:= l) (r:=r) in FIND;auto. + rewrite forallb_forall in ALL1. rewrite Forall_forall. intros. specialize (H _ H0 _ _ (ALL1 _ H0)). destruct x; auto. + apply IHf in ALL2. destruct r; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause