proposition: Lemma chkHc_list_rtrans : forall l1 l2 l', chkHc_list l1 l' = true -> chkHc_list l2 l' = true -> chkHc_list l1 l2 = true.
proof: Proof. intros. eapply forall2b_rtrans; eauto. eapply eq_hc_trans. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause