proposition: Lemma image_true_pr f dom y : forall i, i < dom -> y = f i -> image f dom y = true.
proof: Proof. intros i L E. remember (image f dom y) as b; symmetry in Heqb. destruct b; [ reflexivity | exfalso ]. exfalso; eapply image_false; eauto. Qed.
imports: ZArith Lia MyNat