proposition: Lemma forall2b_rtrans : forall {A: Type} (F : A -> A -> bool) l1 l2 l' (RTRANS : forall x y r, F x r = true -> F y r = true -> F x y = true), forall2b F l1 l' = true -> forall2b F l2 l' = true -> forall2b F l1 l2 = true.
proof: Proof. induction l1 ; simpl. - destruct l' ; try congruence. destruct l2 ; simpl ; congruence. - destruct l' ; try congruence. intros. destruct l2 ; simpl in H0 ; try congruence. rewrite andb_true_iff in *. destruct H. destruct H0. split. eapply RTRANS ; eauto. eapply IHl1 ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause