proposition: Lemma fresh_length : forall L n xs, fresh L n xs -> n = length xs.
proof: Proof. Proof using. intros. gen n L. induction xs; simpl; intros n L Fr; destruct n; tryfalse*. auto. rew_list. rewrite* <- (@IHxs n (L \u \{a})). Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)