proposition: Lemma map_map : forall {A B C: Type} (f: B -> C) (g: A -> B) (a: t A), map f (map g a) = map (fun x => f (g x)) a.
proof: Proof. destruct a. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause