proposition: Lemma make_var : forall b a, make b (var a) <> a -> make (negb b) (var a) = a.
proof: Proof. unfold make. destruct b,a; simpl; congruence. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax