proposition: Lemma is_FF_true : forall f, is_FF f = true -> f = FF.
proof: Proof. destruct f ; simpl; try congruence. destruct l; try congruence. destruct l0 ; try congruence. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause