proposition: Lemma FinSetListCardinality : forall {A : Type} (deqa: Deq A) (l: list A), no_repeats l -> equipollent (FinSetList l) (Fin (length l)).
proof: Proof. Abort. Fixpoint natPrefix (n:nat) := match n with |0 => [] | S m => (natPrefix m) ++ [m] end. Lemma in_app_iff : forall A l l' (a:A), LIn a (l++l') <=> (LIn a l) [+] (LIn a l'). Proof. induction l as [| a l]; introv; simpl; split; introv Hyp; repeat(in_reasoning); try (contradiction); auto. - apply IHl in Hyp. dorn Hyp; auto. - right. apply IHl. auto. - right. apply IHl. auto. Defined.
imports: list