proposition: Lemma fresh_resize_length : forall L n xs, fresh L n xs -> fresh L (length xs) xs.
proof: Proof. Proof using. introv Fr. rewrite* <- (fresh_length _ _ _ Fr). Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)