proposition: Lemma image_true f dom y : image f dom y = true -> { i | i < dom /\ f i = y }.
proof: Proof. induction dom; intros A; dumb. destruct (eq_nat_dec (f dom) y) as [E|E]. exists dom; eauto. destruct IHdom as (i, Hi). simpl in A. auto_if; dumb. exists i; dumb. Defined.
imports: ZArith Lia MyNat