proposition: Lemma fresh_union_r1 : forall xs L1 L2 n, fresh (L1 \u L2) n xs -> fresh L1 n xs.
proof: Proof. Proof using. intros. forwards*: fresh_union_r. Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)