proposition: Lemma eval_or_list'_Exists : forall l, eval_or_list' l <-> Exists eval l.
proof: Proof. induction l. - simpl. intuition. inversion H. - simpl. rewrite IHl ; intuition. inv H1; tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit