proposition: Lemma test_fresh_solve_5 : forall xs L1 n m, m = n -> fresh L1 m xs -> fresh L1 n xs.
proof: Proof. Proof using. intros. fresh_solve. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)