proposition: Lemma has_form_eq : forall m f1 f2 (HASF1: has_form m f1) (HASF2: has_form m f2) (EQ : f1.(id) = f2.(id)), f1 = f2.
proof: Proof. intros m f1. destruct f1 as (i,b,f1). simpl. intros. subst. revert b f2 HASF1 HASF2. assert (SAMELIST : forall l l'0 l0 (H : forall x : t LForm, In x l -> forall (b : bool) (f2 : HFormula), has_form m {| id := id f2; is_dec := b; elt := elt x |} -> has_form m f2 -> {| id := id f2; is_dec := b; elt := elt x |} = f2) (H4 : Forall (has_form m) l) (H6 : chkHc_list l l'0 = true) (H0 : Forall (has_form m) l0) (H2 : chkHc_list l0 l'0 = true), Forall2 eq l l0). { intros. specialize (chkHc_list_rtrans _ _ _ H6 H2). intro. apply forall2b_Forall2 in H1. clear H6 H2. induction H1. + constructor. + apply Forall_rew in H4. apply Forall_rew in H0. unfold eq_hc in H1. rewrite andb_true_iff in H1. rewrite Bool.eqb_true_iff in H1. destruct H1 ; subst. assert (id x = id y) by lia. constructor. * destruct x. simpl in H5. subst. apply (H {| id := id y ; is_dec := is_dec0 ; elt := elt0 |}). simpl. tauto. tauto. tauto. * apply IHForall2; try tauto. intros. eapply H ; eauto. simpl. tauto. } induction f1 using form_ind. - intros. inv HASF1. inv HASF2; simpl in * ; congruence. - intros. inv HASF1. inv HASF2; simpl in *; try congruence. rewrite H5 in H1. inv H1. f_equal. f_equal. apply forall2_eq_list. eapply SAMELIST; eauto. - intros. inv HASF1. inv HASF2; simpl in *; try congruence. rewrite H6 in H2. inv H2. f_equal. f_equal. apply forall2_eq_list. eapply SAMELIST;eauto. eauto. specialize (eq_hc_trans H8 H9). intro. unfold eq_hc in H2. rewrite andb_true_iff in H2. rewrite Bool.eqb_true_iff in H2. destruct H2. assert (id r = id r0) by (clear - H2; lia). destruct r. simpl in *. subst. apply IHf1;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause