proposition: Lemma img_singles_incl : forall xs vs, List.incl (img (xs ∷ vs)) vs.
proof: Proof. induction xs; induction vs; intros; simpl; auto. apply incl_refl. unfold List.incl; intros x Hin; inversion Hin. apply incl_refl. apply List.incl_cons. simpl; auto. apply List.incl_tl. auto. Qed.
imports: Utf8 Equalities