proposition: Lemma is_TT_true : forall f, is_TT f = true -> f = TT.
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