proposition: Lemma test_fresh_solve_3 : forall xs L1 L2 n, fresh (L1 \u L2) n xs -> fresh \{} n xs.
proof: Proof. Proof using. intros. fresh_solve. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)