proposition: Lemma img_singles : forall xs vs, length xs = length vs -> img (xs ∷ vs) = vs.
proof: Proof. induction xs as [ | x xs IHxs ]; induction vs; intro Hlen; inversion Hlen as [ Hlen2 ]; auto. simpl. rewrite (IHxs vs Hlen2); auto. Qed.
imports: Utf8 Equalities